λδ-2B is released

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / cpxs_teqx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqx.ma
index 7af7b41b8aef9be884f43f5a5560a1e20d11cc20..178a2c440e8e29c742db8e99e30efe37bcd6606a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqx.ma
@@ -19,7 +19,7 @@ include "basic_2/rt_computation/cpxs.ma".
 
 (* Properties with sort-irrelevant equivalence for terms ********************)
 
-lemma teqx_cpxs_trans: ∀h,U1,T1. U1 ≛ T1 → ∀G,L,T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → 
+lemma teqx_cpxs_trans: ∀h,U1,T1. U1 ≛ T1 → ∀G,L,T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 →
                        ∃∃U2. ⦃G,L⦄ ⊢ U1 ⬈*[h] U2 & U2 ≛ T2.
 #h #U1 #T1 #HUT1 #G #L #T2 #HT12 @(cpxs_ind … HT12) -T2 /2 width=3 by ex2_intro/
 #T #T2 #_ #HT2 * #U #HU1 #HUT elim (teqx_cpx_trans … HUT … HT2) -T -T1