advances on ldrop ....

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

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 18744a5397aa819f988434ff6c36de171c3d9dfb..c54215e60149917f169fbed91d7558318a464413 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma
@@ -13,18 +13,18 @@
 (**************************************************************************)
 
 include "basic_2/substitution/fqus_alt.ma".
-include "basic_2/substitution/lleq_ext.ma".
+include "basic_2/substitution/lleq_ldrop.ma".
 
 (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
 
-(* Properties on supclosure and derivatives *********************************)
+(* Properties on supclosure *************************************************)
 
-lemma lleq_fqu_trans: â\88\80G1,G2,L2,K2,T,U. â¦\83G1, L2, Tâ¦\84 â\8a\83 ⦃G2, K2, U⦄ →
-                      â\88\80L1. L1 â\8b\95[T, 0] L2 →
-                      â\88\83â\88\83K1. â¦\83G1, L1, Tâ¦\84 â\8a\83 â¦\83G2, K1, Uâ¦\84 & K1 â\8b\95[U, 0] K2.
+lemma lleq_fqu_trans: â\88\80G1,G2,L2,K2,T,U. â¦\83G1, L2, Tâ¦\84 â\8a\90 ⦃G2, K2, U⦄ →
+                      â\88\80L1. L1 â\89¡[T, 0] L2 →
+                      â\88\83â\88\83K1. â¦\83G1, L1, Tâ¦\84 â\8a\90 â¦\83G2, K1, Uâ¦\84 & K1 â\89¡[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 //
-  #I1 #K1 #H1 #H2 lapply (ldrop_inv_O2 … H1) -H1
+  #K1 #H1 #H2 lapply (ldrop_inv_O2 … H1) -H1
   #H destruct /2 width=3 by fqu_lref_O, ex2_intro/
 | * [ #a ] #I #G #L2 #V #T #L1 #H
   [ elim (lleq_inv_bind … H)
@@ -36,7 +36,7 @@ lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃ ⦃G2, K2, U⦄ 
 | #I #G #L2 #V #T #L1 #H elim (lleq_inv_flat … H) -H
   /2 width=3 by fqu_flat_dx, ex2_intro/
 | #G #L2 #K2 #T #U #e #HLK2 #HTU #L1 #HL12
-  elim (ldrop_O1_le (e+1) L1)
+  elim (ldrop_O1_le (Ⓕ) (e+1) L1)
   [ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/
   | lapply (ldrop_fwd_length_le2 … HLK2) -K2
     lapply (lleq_fwd_length … HL12) -T -U //
@@ -44,18 +44,18 @@ lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃ ⦃G2, K2, U⦄ 
 ]
 qed-.
 
-lemma lleq_fquq_trans: â\88\80G1,G2,L2,K2,T,U. â¦\83G1, L2, Tâ¦\84 â\8a\83⸮ ⦃G2, K2, U⦄ →
-                       â\88\80L1. L1 â\8b\95[T, 0] L2 →
-                       â\88\83â\88\83K1. â¦\83G1, L1, Tâ¦\84 â\8a\83⸮ â¦\83G2, K1, Uâ¦\84 & K1 â\8b\95[U, 0] K2.
+lemma lleq_fquq_trans: â\88\80G1,G2,L2,K2,T,U. â¦\83G1, L2, Tâ¦\84 â\8a\90⸮ ⦃G2, K2, U⦄ →
+                       â\88\80L1. L1 â\89¡[T, 0] L2 →
+                       â\88\83â\88\83K1. â¦\83G1, L1, Tâ¦\84 â\8a\90⸮ â¦\83G2, K1, Uâ¦\84 & K1 â\89¡[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/
 ]
 qed-.
 
-lemma lleq_fqup_trans: â\88\80G1,G2,L2,K2,T,U. â¦\83G1, L2, Tâ¦\84 â\8a\83+ ⦃G2, K2, U⦄ →
-                       â\88\80L1. L1 â\8b\95[T, 0] L2 →
-                       â\88\83â\88\83K1. â¦\83G1, L1, Tâ¦\84 â\8a\83+ â¦\83G2, K1, Uâ¦\84 & K1 â\8b\95[U, 0] K2.
+lemma lleq_fqup_trans: â\88\80G1,G2,L2,K2,T,U. â¦\83G1, L2, Tâ¦\84 â\8a\90+ ⦃G2, K2, U⦄ →
+                       â\88\80L1. L1 â\89¡[T, 0] L2 →
+                       â\88\83â\88\83K1. â¦\83G1, L1, Tâ¦\84 â\8a\90+ â¦\83G2, K1, Uâ¦\84 & K1 â\89¡[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/
@@ -65,9 +65,9 @@ lemma lleq_fqup_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃+ ⦃G2, K2, U⦄
 ]
 qed-.
 
-lemma lleq_fqus_trans: â\88\80G1,G2,L2,K2,T,U. â¦\83G1, L2, Tâ¦\84 â\8a\83* ⦃G2, K2, U⦄ →
-                       â\88\80L1. L1 â\8b\95[T, 0] L2 →
-                       â\88\83â\88\83K1. â¦\83G1, L1, Tâ¦\84 â\8a\83* â¦\83G2, K1, Uâ¦\84 & K1 â\8b\95[U, 0] K2.
+lemma lleq_fqus_trans: â\88\80G1,G2,L2,K2,T,U. â¦\83G1, L2, Tâ¦\84 â\8a\90* ⦃G2, K2, U⦄ →
+                       â\88\80L1. L1 â\89¡[T, 0] L2 →
+                       â\88\83â\88\83K1. â¦\83G1, L1, Tâ¦\84 â\8a\90* â¦\83G2, K1, Uâ¦\84 & K1 â\89¡[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/