- degree-based equivalene for terms

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / drops_lreq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma
index c6899fd3effa741504a8ab75355b618792b35f52..c9934f66450fd0686db6bdc11e79e66d2f7d3492 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma
@@ -21,8 +21,7 @@ include "basic_2/relocation/drops_lexs.ma".
 
 lemma lreq_co_dedropable: co_dedropable_sn lreq.
 @lexs_liftable_co_dedropable
-/2 width=6 by cfull_lift, ceq_lift, cfull_refl, ceq_refl/
-qed-.
+/2 width=6 by cfull_lift, ceq_lift/ qed-.
 
 lemma lreq_co_dropable_sn: co_dropable_sn lreq.
 @lexs_co_dropable_sn qed-.
@@ -56,5 +55,4 @@ lemma drops_lreq_trans_next: ∀f1,K1,K2. K1 ≡[f1] K2 →
                              ∃∃L2. ⬇*[b,f] L2.ⓑ{I}V ≡ K2 & L1 ≡[f2] L2 & L1.ⓑ{I}V ≡[f] L2.ⓑ{I}V.
 #f1 #K1 #K2 #HK12 #b #f #I #L1 #V #HLK1 #f2 #Hf2
 elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -f1 -K1
-/2 width=6 by cfull_lift, ceq_lift, cfull_refl, ceq_refl, ex3_intro/
-qed-.
+/2 width=6 by cfull_lift, ceq_lift, ex3_intro/ qed-.