-lemma cpx_delift: ∀h,o,I,G,K,V,T1,L,l. ⬇[l] L ≡ (K.ⓑ{I}V) →
- ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 & ⬆[l, 1] T ≡ T2.
-#h #o #I #G #K #V #T1 elim T1 -T1
-[ * #i #L #l /2 width=4 by cpx_atom, lift_sort, lift_gref, ex2_2_intro/
- elim (lt_or_eq_or_gt i l) #Hil [1,3: /4 width=4 by cpx_atom, lift_lref_ge_minus, lift_lref_lt, ylt_inj, yle_inj, ex2_2_intro/ ]
- destruct
- elim (lift_total V 0 (i+1)) #W #HVW
- elim (lift_split … HVW i i) /3 width=7 by cpx_delta, ex2_2_intro/
-| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #l #HLK
- elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
- [ elim (IHU1 (L. ⓑ{I} W1) (l+1)) -IHU1 /3 width=9 by cpx_bind, drop_drop, lift_bind, ex2_2_intro/
- | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpx_flat, lift_flat, ex2_2_intro/
- ]
-]
-qed-.
+lemma cpx_flat: ∀h,I,G,L,V1,V2,T1,T2.
+ ⦃G,L⦄ ⊢ V1 ⬈[h] V2 → ⦃G,L⦄ ⊢ T1 ⬈[h] T2 →
+ ⦃G,L⦄ ⊢ ⓕ{I}V1.T1 ⬈[h] ⓕ{I}V2.T2.
+#h * #G #L #V1 #V2 #T1 #T2 * #cV #HV12 *
+/3 width=5 by cpg_appl, cpg_cast, ex_intro/
+qed.
+
+lemma cpx_zeta (h) (G) (L):
+ ∀T1,T. ⬆*[1] T ≘ T1 → ∀T2. ⦃G,L⦄ ⊢ T ⬈[h] T2 →
+ ∀V. ⦃G,L⦄ ⊢ +ⓓV.T1 ⬈[h] T2.
+#h #G #L #T1 #T #HT1 #T2 *
+/3 width=4 by cpg_zeta, ex_intro/
+qed.
+
+lemma cpx_eps: ∀h,G,L,V,T1,T2. ⦃G,L⦄ ⊢ T1 ⬈[h] T2 → ⦃G,L⦄ ⊢ ⓝV.T1 ⬈[h] T2.
+#h #G #L #V #T1 #T2 *
+/3 width=2 by cpg_eps, ex_intro/
+qed.
+
+(* Basic_2A1: was: cpx_ct *)
+lemma cpx_ee: ∀h,G,L,V1,V2,T. ⦃G,L⦄ ⊢ V1 ⬈[h] V2 → ⦃G,L⦄ ⊢ ⓝV1.T ⬈[h] V2.
+#h #G #L #V1 #V2 #T *
+/3 width=2 by cpg_ee, ex_intro/
+qed.
+
+lemma cpx_beta: ∀h,p,G,L,V1,V2,W1,W2,T1,T2.
+ ⦃G,L⦄ ⊢ V1 ⬈[h] V2 → ⦃G,L⦄ ⊢ W1 ⬈[h] W2 → ⦃G,L.ⓛW1⦄ ⊢ T1 ⬈[h] T2 →
+ ⦃G,L⦄ ⊢ ⓐV1.ⓛ{p}W1.T1 ⬈[h] ⓓ{p}ⓝW2.V2.T2.
+#h #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 * #cV #HV12 * #cW #HW12 *
+/3 width=2 by cpg_beta, ex_intro/
+qed.
+
+lemma cpx_theta: ∀h,p,G,L,V1,V,V2,W1,W2,T1,T2.
+ ⦃G,L⦄ ⊢ V1 ⬈[h] V → ⬆*[1] V ≘ V2 → ⦃G,L⦄ ⊢ W1 ⬈[h] W2 →
+ ⦃G,L.ⓓW1⦄ ⊢ T1 ⬈[h] T2 →
+ ⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ⬈[h] ⓓ{p}W2.ⓐV2.T2.
+#h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 * #cV #HV1 #HV2 * #cW #HW12 *
+/3 width=4 by cpg_theta, ex_intro/
+qed.
+
+(* Basic_2A1: includes: cpx_atom *)
+lemma cpx_refl: ∀h,G,L. reflexive … (cpx h G L).
+/3 width=2 by cpg_refl, ex_intro/ qed.
+
+(* Advanced properties ******************************************************)
+
+lemma cpx_pair_sn: ∀h,I,G,L,V1,V2. ⦃G,L⦄ ⊢ V1 ⬈[h] V2 →
+ ∀T. ⦃G,L⦄ ⊢ ②{I}V1.T ⬈[h] ②{I}V2.T.
+#h * /2 width=2 by cpx_flat, cpx_bind/
+qed.
+
+lemma cpg_cpx (h) (Rt) (c) (G) (L):
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬈[Rt,c,h] T2 → ⦃G,L⦄ ⊢ T1 ⬈[h] T2.
+#h #Rt #c #G #L #T1 #T2 #H elim H -c -G -L -T1 -T2
+/2 width=3 by cpx_theta, cpx_beta, cpx_ee, cpx_eps, cpx_zeta, cpx_flat, cpx_bind, cpx_lref, cpx_delta/
+qed.