X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Flsubv_drops.ma;h=06d302d57df17dbc634d0e0e7708f8d76023c75b;hp=90b59cba0bafca1100c0c9450418c601c4110973;hb=1083ac3b1acac5f1ac1fa40a9a417dd9d268dced;hpb=93768d9ebc0e3c8e3bcd69571d7a635cb1a16b29

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma
index 90b59cba0..06d302d57 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma
@@ -34,7 +34,7 @@ lemma lsubv_drops_conf_isuni (a) (h) (G):
   | #g #Hg #HLK1 #H destruct -HL12
     elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
   ]
-| #L1 #L2 #W #V #HVW #HW #HL12 #IH #b #f #K1 #Hf #H
+| #L1 #L2 #W #V #HVW #HL12 #IH #b #f #K1 #Hf #H
   elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
   [ #Hf #H destruct -IH
     /3 width=3 by drops_refl, lsubv_beta, ex2_intro/
@@ -59,7 +59,7 @@ lemma lsubv_drops_trans_isuni (a) (h) (G):
   | #g #Hg #HLK2 #H destruct -HL12
     elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
   ]
-| #L1 #L2 #W #V #HWV #HW #HL12 #IH #b #f #K2 #Hf #H
+| #L1 #L2 #W #V #HWV #HL12 #IH #b #f #K2 #Hf #H
   elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
   [ #Hf #H destruct -IH
     /3 width=3 by drops_refl, lsubv_beta, ex2_intro/