X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Ffqus_alt.ma;h=2681a04acc346b22be68af233b67a179a811559f;hb=02df4ecb9d5ad173a3e306952cc09d83b62cfdcf;hp=0d8241111a709b156b8f3060a3e73984b88e993a;hpb=7a112c2797e15ccd67bcbd7308fddcc54bff60ed;p=helm.git

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 0d8241111..2681a04ac 100644
--- 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⦄ →
-                       ∀G2,L2,T2. ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
-#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-.