X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Flleq_fqus.ma;h=ac1329b4530767e88b9a6363e0bf40f095eff7b3;hb=7a25b8fcba2436a75556db1725c6e1be78a9faca;hp=3a510eb28c9445822d375bcee3479f4355db4b51;hpb=6aab24b40d5d09561375959043ecd85c8b428d85;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma
index 3a510eb28..ac1329b45 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma
@@ -20,8 +20,8 @@ include "basic_2/substitution/lleq_ldrop.ma".
 (* Properties on supclosure *************************************************)
 
 lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐ ⦃G2, K2, U⦄ →
-                      ∀L1. L1 ⋕[T, 0] L2 →
-                      ∃∃K1. ⦃G1, L1, T⦄ ⊐ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2.
+                      ∀L1. L1 ≡[T, 0] L2 →
+                      ∃∃K1. ⦃G1, L1, T⦄ ⊐ ⦃G2, K1, U⦄ & K1 ≡[U, 0] K2.
 #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U
 [ #I #G #L2 #V #L1 #H elim (lleq_inv_lref_ge_dx … H … I L2 V) -H //
   #K1 #H1 #H2 lapply (ldrop_inv_O2 … H1) -H1
@@ -45,8 +45,8 @@ lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐ ⦃G2, K2, U⦄ 
 qed-.
 
 lemma lleq_fquq_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐⸮ ⦃G2, K2, U⦄ →
-                       ∀L1. L1 ⋕[T, 0] L2 →
-                       ∃∃K1. ⦃G1, L1, T⦄ ⊐⸮ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2.
+                       ∀L1. L1 ≡[T, 0] L2 →
+                       ∃∃K1. ⦃G1, L1, T⦄ ⊐⸮ ⦃G2, K1, U⦄ & K1 ≡[U, 0] K2.
 #G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fquq_inv_gen … H) -H
 [ #H elim (lleq_fqu_trans … H … HL12) -L2 /3 width=3 by fqu_fquq, ex2_intro/
 | * #HG #HL #HT destruct /2 width=3 by ex2_intro/
@@ -54,8 +54,8 @@ lemma lleq_fquq_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐⸮ ⦃G2, K2, U
 qed-.
 
 lemma lleq_fqup_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐+ ⦃G2, K2, U⦄ →
-                       ∀L1. L1 ⋕[T, 0] L2 →
-                       ∃∃K1. ⦃G1, L1, T⦄ ⊐+ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2.
+                       ∀L1. L1 ≡[T, 0] L2 →
+                       ∃∃K1. ⦃G1, L1, T⦄ ⊐+ ⦃G2, K1, U⦄ & K1 ≡[U, 0] K2.
 #G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U
 [ #G2 #K2 #U #HTU #L1 #HL12 elim (lleq_fqu_trans … HTU … HL12) -L2
   /3 width=3 by fqu_fqup, ex2_intro/
@@ -66,8 +66,8 @@ lemma lleq_fqup_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐+ ⦃G2, K2, U⦄
 qed-.
 
 lemma lleq_fqus_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐* ⦃G2, K2, U⦄ →
-                       ∀L1. L1 ⋕[T, 0] L2 →
-                       ∃∃K1. ⦃G1, L1, T⦄ ⊐* ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2.
+                       ∀L1. L1 ≡[T, 0] L2 →
+                       ∃∃K1. ⦃G1, L1, T⦄ ⊐* ⦃G2, K1, U⦄ & K1 ≡[U, 0] K2.
 #G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_gen … H) -H
 [ #H elim (lleq_fqup_trans … H … HL12) -L2 /3 width=3 by fqup_fqus, ex2_intro/
 | * #HG #HL #HT destruct /2 width=3 by ex2_intro/