- bug fix in the induction for the closure property

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / fqus_alt.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_alt.ma
index 0d8241111a709b156b8f3060a3e73984b88e993a..2681a04acc346b22be68af233b67a179a811559f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_alt.ma
@@ -54,8 +54,8 @@ lemma fqus_fqup_trans: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G, L
 /2 width=5 by fqus_strap1_fqu, fqup_strap1/
 qed-.
 
-lemma fqup_fqus_trans: ∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ →
-                       â\88\80G2,L2,T2. â¦\83G, L, Tâ¦\84 â\8a\83* â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 â\8a\83+ â¦\83G2, L2, T2â¦\84.
-#G1 #G #L1 #L #T1 #T #H1 @(fqup_ind_dx … H1) -H1 -G1 -L1 -T1
+lemma fqup_fqus_trans: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ →
+                       ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
+#G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 @(fqup_ind_dx … H1) -H1 -G1 -L1 -T1
 /3 width=5 by fqus_strap2_fqu, fqup_strap2/
 qed-.