update in ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / lsubv_drops.ma

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 90b59cba0bafca1100c0c9450418c601c4110973..06d302d57df17dbc634d0e0e7708f8d76023c75b 100644 (file)
--- 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/