still more additions and corrections for the article

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / lsubr_lsubr.ma

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 3bf83b81ebbaa24ac43ceb607e30a2862673ebc3..2aba1cf65eb79b5fc97aae082875349614cac1f6 100644 (file)
--- 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-.