X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Flsubr_lsubr.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Flsubr_lsubr.ma;h=2aba1cf65eb79b5fc97aae082875349614cac1f6;hb=f76594123e375bd7852c9421fe260a7bec693a92;hp=3bf83b81ebbaa24ac43ceb607e30a2862673ebc3;hpb=a454837a256907d2f83d42ced7be847e10361ea9;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/lsubr_lsubr.ma b/matita/matita/contribs/lambdadelta/static_2/static/lsubr_lsubr.ma
index 3bf83b81e..2aba1cf65 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/lsubr_lsubr.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/lsubr_lsubr.ma
@@ -21,12 +21,12 @@ include "static_2/static/lsubr.ma".
 theorem lsubr_trans: Transitive … lsubr.
 #L1 #L #H elim H -L1 -L //
 [ #I #L1 #L #_ #IH #X #H elim (lsubr_inv_bind1 … H) -H *
-  [ #L2 #HL2 #H | #L2 #V #W #HL2 #H1 #H2 | #I1 #I2 #L2 #V #Hl2 #H1 #H2 ]
+  [ #L2 #HL2 #H | #L2 #V #W #HL2 #H1 #H2 | #I1 #I2 #L2 #V #HL2 #H1 #H2 ]
   destruct /3 width=1 by lsubr_bind, lsubr_beta, lsubr_unit/
 | #L1 #L #V #W #_ #IH #X #H elim (lsubr_inv_abst1 … H) -H *
   [ #L2 #HL2 #H | #I #L2 #HL2 #H ]
   destruct /3 width=1 by lsubr_beta, lsubr_unit/
 | #I1 #I2 #L1 #L #V #_ #IH #X #H elim (lsubr_inv_unit1 … H) -H
-  /4 width=1 by lsubr_unit/
+  #L2 #HL2 #H destruct /4 width=1 by lsubr_unit/
 ]
 qed-.