(* Properties on supclosure *************************************************)
-lemma aaa_fqu_conf: â\88\80G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â\8a\90 â¦\83G2,L2,T2â¦\84 →
- â\88\80A1. â¦\83G1,L1â¦\84 â\8a¢ T1 â\81\9d A1 â\86\92 â\88\83A2. â¦\83G2,L2â¦\84 ⊢ T2 ⁝ A2.
+lemma aaa_fqu_conf: â\88\80G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82 â\9d¨G2,L2,T2â\9d© →
+ â\88\80A1. â\9d¨G1,L1â\9d© â\8a¢ T1 â\81\9d A1 â\86\92 â\88\83A2. â\9d¨G2,L2â\9d© ⊢ T2 ⁝ A2.
#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
[ #I #G #L #T #A #H elim (aaa_inv_zero … H) -H
#J #K #V #H #HA destruct /2 width=2 by ex_intro/
| elim (aaa_inv_appl … H)
| elim (aaa_inv_cast … H)
] -H /2 width=2 by ex_intro/
-| #p * #G #L #V #T #X #H
+| #p * #G #L #V #T #_ #X #H
[ elim (aaa_inv_abbr … H)
| elim (aaa_inv_abst … H)
] -H /2 width=2 by ex_intro/
]
qed-.
-lemma aaa_fquq_conf: â\88\80G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â\8a\90⸮ â¦\83G2,L2,T2â¦\84 →
- â\88\80A1. â¦\83G1,L1â¦\84 â\8a¢ T1 â\81\9d A1 â\86\92 â\88\83A2. â¦\83G2,L2â¦\84 ⊢ T2 ⁝ A2.
+lemma aaa_fquq_conf: â\88\80G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82⸮ â\9d¨G2,L2,T2â\9d© →
+ â\88\80A1. â\9d¨G1,L1â\9d© â\8a¢ T1 â\81\9d A1 â\86\92 â\88\83A2. â\9d¨G2,L2â\9d© ⊢ T2 ⁝ A2.
#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H /2 width=6 by aaa_fqu_conf/
* #H1 #H2 #H3 destruct /2 width=2 by ex_intro/
qed-.
-lemma aaa_fqup_conf: â\88\80G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â\8a\90+ â¦\83G2,L2,T2â¦\84 →
- â\88\80A1. â¦\83G1,L1â¦\84 â\8a¢ T1 â\81\9d A1 â\86\92 â\88\83A2. â¦\83G2,L2â¦\84 ⊢ T2 ⁝ A2.
+lemma aaa_fqup_conf: â\88\80G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82+ â\9d¨G2,L2,T2â\9d© →
+ â\88\80A1. â\9d¨G1,L1â\9d© â\8a¢ T1 â\81\9d A1 â\86\92 â\88\83A2. â\9d¨G2,L2â\9d© ⊢ T2 ⁝ A2.
#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
[2: #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #A #HA elim (IH1 … HA) -IH1 -A ]
/2 width=6 by aaa_fqu_conf/
qed-.
-lemma aaa_fqus_conf: â\88\80G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â\8a\90* â¦\83G2,L2,T2â¦\84 →
- â\88\80A1. â¦\83G1,L1â¦\84 â\8a¢ T1 â\81\9d A1 â\86\92 â\88\83A2. â¦\83G2,L2â¦\84 ⊢ T2 ⁝ A2.
+lemma aaa_fqus_conf: â\88\80G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82* â\9d¨G2,L2,T2â\9d© →
+ â\88\80A1. â\9d¨G1,L1â\9d© â\8a¢ T1 â\81\9d A1 â\86\92 â\88\83A2. â\9d¨G2,L2â\9d© ⊢ T2 ⁝ A2.
#G1 #G2 #L1 #L2 #T1 #T2 #H elim(fqus_inv_fqup … H) -H /2 width=6 by aaa_fqup_conf/
* #H1 #H2 #H3 destruct /2 width=2 by ex_intro/
qed-.