(* Properties on basic relocation *******************************************)
-lemma aaa_lift: â\88\80G,L1,T1,A. â¦\83G, L1â¦\84 â\8a¢ T1 â\81\9d A â\86\92 â\88\80L2,s,d,e. â\87©[s, d, e] L2 ≡ L1 →
- â\88\80T2. â\87§[d, e] T1 ≡ T2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
+lemma aaa_lift: â\88\80G,L1,T1,A. â¦\83G, L1â¦\84 â\8a¢ T1 â\81\9d A â\86\92 â\88\80L2,s,d,e. â¬\87[s, d, e] L2 ≡ L1 →
+ â\88\80T2. â¬\86[d, e] T1 ≡ T2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
#G #L1 #T1 #A #H elim H -G -L1 -T1 -A
[ #G #L1 #k #L2 #s #d #e #_ #T2 #H
>(lift_inv_sort1 … H) -H //
]
qed.
-lemma aaa_inv_lift: â\88\80G,L2,T2,A. â¦\83G, L2â¦\84 â\8a¢ T2 â\81\9d A â\86\92 â\88\80L1,s,d,e. â\87©[s, d, e] L2 ≡ L1 →
- â\88\80T1. â\87§[d, e] T1 ≡ T2 → ⦃G, L1⦄ ⊢ T1 ⁝ A.
+lemma aaa_inv_lift: â\88\80G,L2,T2,A. â¦\83G, L2â¦\84 â\8a¢ T2 â\81\9d A â\86\92 â\88\80L1,s,d,e. â¬\87[s, d, e] L2 ≡ L1 →
+ â\88\80T1. â¬\86[d, e] T1 ≡ T2 → ⦃G, L1⦄ ⊢ T1 ⁝ A.
#G #L2 #T2 #A #H elim H -G -L2 -T2 -A
[ #G #L2 #k #L1 #s #d #e #_ #T1 #H
>(lift_inv_sort2 … H) -H //