(* Properties on supclosure *************************************************)
-lemma lleq_fqu_trans: â\88\80G1,G2,L2,K2,T,U. â¦\83G1, L2, Tâ¦\84 â\8a\83 ⦃G2, K2, U⦄ →
+lemma lleq_fqu_trans: â\88\80G1,G2,L2,K2,T,U. â¦\83G1, L2, Tâ¦\84 â\8a\90 ⦃G2, K2, U⦄ →
∀L1. L1 ⋕[T, 0] L2 →
- â\88\83â\88\83K1. â¦\83G1, L1, Tâ¦\84 â\8a\83 ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2.
+ â\88\83â\88\83K1. â¦\83G1, L1, Tâ¦\84 â\8a\90 ⦃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
]
qed-.
-lemma lleq_fquq_trans: â\88\80G1,G2,L2,K2,T,U. â¦\83G1, L2, Tâ¦\84 â\8a\83⸮ ⦃G2, K2, U⦄ →
+lemma lleq_fquq_trans: â\88\80G1,G2,L2,K2,T,U. â¦\83G1, L2, Tâ¦\84 â\8a\90⸮ ⦃G2, K2, U⦄ →
∀L1. L1 ⋕[T, 0] L2 →
- â\88\83â\88\83K1. â¦\83G1, L1, Tâ¦\84 â\8a\83⸮ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2.
+ â\88\83â\88\83K1. â¦\83G1, L1, Tâ¦\84 â\8a\90⸮ ⦃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/
]
qed-.
-lemma lleq_fqup_trans: â\88\80G1,G2,L2,K2,T,U. â¦\83G1, L2, Tâ¦\84 â\8a\83+ ⦃G2, K2, U⦄ →
+lemma lleq_fqup_trans: â\88\80G1,G2,L2,K2,T,U. â¦\83G1, L2, Tâ¦\84 â\8a\90+ ⦃G2, K2, U⦄ →
∀L1. L1 ⋕[T, 0] L2 →
- â\88\83â\88\83K1. â¦\83G1, L1, Tâ¦\84 â\8a\83+ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2.
+ â\88\83â\88\83K1. â¦\83G1, L1, Tâ¦\84 â\8a\90+ ⦃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/
]
qed-.
-lemma lleq_fqus_trans: â\88\80G1,G2,L2,K2,T,U. â¦\83G1, L2, Tâ¦\84 â\8a\83* ⦃G2, K2, U⦄ →
+lemma lleq_fqus_trans: â\88\80G1,G2,L2,K2,T,U. â¦\83G1, L2, Tâ¦\84 â\8a\90* ⦃G2, K2, U⦄ →
∀L1. L1 ⋕[T, 0] L2 →
- â\88\83â\88\83K1. â¦\83G1, L1, Tâ¦\84 â\8a\83* ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2.
+ â\88\83â\88\83K1. â¦\83G1, L1, Tâ¦\84 â\8a\90* ⦃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/