(* Properties with atomic arity assignment for terms ************************)
(* Note: lemma 500 *)
-(* Basic_2A1: was: cpx_lpx_aaa_conf *)
+(* Basic_2A1: uses: cpx_lpx_aaa_conf *)
lemma cpx_aaa_conf_lfpx: ∀h,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A →
∀T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 →
∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T1] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
[ #H destruct /3 width=1 by aaa_zero/
| -HV12 * /4 width=7 by aaa_lifts, drops_refl, drops_drop/
]
-| #I #G #L1 #V1 #B #i #_ #IH #X2 #HX #Y #HY
- elim (lfpx_inv_lref_pair_sn … HY) -HY #L2 #W2 #HL12 #H destruct
- elim (cpx_inv_lref1_pair … HX) -HX
+| #I #G #L1 #B #i #_ #IH #X2 #HX #Y #HY
+ elim (lfpx_inv_lref_bind_sn … HY) -HY #I2 #L2 #HL12 #H destruct
+ elim (cpx_inv_lref1_bind … HX) -HX
[ #H destruct /3 width=1 by aaa_lref/
| * /4 width=7 by aaa_lifts, drops_refl, drops_drop/
]
elim (lfpx_inv_bind … HL12) -HL12 #HV #HT
elim (cpx_inv_abbr1 … HX) -HX *
[ #V2 #T2 #HV12 #HT12 #H destruct
- /4 width=2 by lfpx_pair_repl_dx, aaa_abbr/
+ /5 width=2 by lfpx_bind_repl_dx, aaa_abbr, ext2_pair/
| #T2 #HT12 #HXT2 #H destruct -IHV
/4 width=7 by aaa_inv_lifts, drops_drop, drops_refl/
]
| #p #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X2 #H #L2 #HL12
elim (lfpx_inv_bind … HL12) -HL12 #HV #HT
elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- /4 width=2 by lfpx_pair_repl_dx, aaa_abst/
+ /5 width=2 by lfpx_bind_repl_dx, aaa_abst, ext2_pair/
| #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X2 #H #L2 #HL12
elim (lfpx_inv_flat … HL12) -HL12 #HV #HT
elim (cpx_inv_appl1 … H) -H *
]
qed-.
-lemma cpx_aaa_conf: ∀h,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A →
- ∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+lemma cpx_aaa_conf: ∀h,G,L. Conf3 … (aaa G L) (cpx h G L).
/2 width=6 by cpx_aaa_conf_lfpx/ qed-.
-lemma lfpx_aaa_conf: ∀h,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
- ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+(* Basic_2A1: uses: lpx_aaa_conf *)
+lemma lfpx_aaa_conf: ∀h,G,T. Conf3 … (λL. aaa G L T) (lfpx h G T).
/2 width=6 by cpx_aaa_conf_lfpx/ qed-.