- lambdadelta: first recursive part of preservation finally proved!

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / unfold / ldrops.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops.ma
index b899bd27383e2db78271ed88b6cc4210d522a1d3..9af21a0f152ff321fcc60c5735c0a45e8b61a44a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops.ma
@@ -86,5 +86,4 @@ lemma ldrops_skip: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2
 ].
 qed.
 
-(* Basic_1: removed theorems 1: drop1_getl_trans
-*)
+(* Basic_1: removed theorems 1: drop1_getl_trans *)