/3 width=3 by cpm_cpms, ex2_intro/ qed-.
fact cnv_cpm_conf_lpr_atom_delta_aux (h) (a) (G) (L) (i):
- (∀G0,L0,T0. ❪G,L,#i❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,#i❫ > ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
❪G,L❫⊢#i![h,a] →
∀K,V. ⇩[i]L ≘ K.ⓓV →
∀n,XV. ❪G,K❫ ⊢ V ➡[h,n] XV →
qed-.
fact cnv_cpm_conf_lpr_atom_ell_aux (h) (a) (G) (L) (i):
- (∀G0,L0,T0. ❪G,L,#i❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,#i❫ > ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
❪G,L❫⊢#i![h,a] →
∀K,W. ⇩[i]L ≘ K.ⓛW →
∀n,XW. ❪G,K❫ ⊢ W ➡[h,n] XW →
qed-.
fact cnv_cpm_conf_lpr_delta_delta_aux (h) (a) (I) (G) (L) (i):
- (∀G0,L0,T0. ❪G,L,#i❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,#i❫ > ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
❪G,L❫⊢#i![h,a] →
∀K1,V1. ⇩[i]L ≘ K1.ⓑ[I]V1 → ∀K2,V2. ⇩[i]L ≘ K2.ⓑ[I]V2 →
∀n1,XV1. ❪G,K1❫ ⊢ V1 ➡[h,n1] XV1 → ∀n2,XV2. ❪G,K2❫ ⊢ V2 ➡[h,n2] XV2 →
qed-.
fact cnv_cpm_conf_lpr_bind_bind_aux (h) (a) (p) (I) (G) (L) (V) (T):
- (∀G0,L0,T0. ❪G,L,ⓑ[p,I]V.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,ⓑ[p,I]V.T❫ > ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
❪G,L❫ ⊢ ⓑ[p,I]V.T ![h,a] →
∀V1. ❪G,L❫ ⊢ V ➡[h,0] V1 → ∀V2. ❪G,L❫ ⊢ V ➡[h,0] V2 →
∀n1,T1. ❪G,L.ⓑ[I]V❫ ⊢ T ➡[h,n1] T1 → ∀n2,T2. ❪G,L.ⓑ[I]V❫ ⊢ T ➡[h,n2] T2 →
qed-.
fact cnv_cpm_conf_lpr_bind_zeta_aux (h) (a) (G) (L) (V) (T):
- (∀G0,L0,T0. ❪G,L,+ⓓV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,+ⓓV.T❫ > ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
❪G,L❫ ⊢ +ⓓV.T ![h,a] →
∀V1. ❪G,L❫ ⊢V ➡[h,0] V1 → ∀n1,T1. ❪G,L.ⓓV❫ ⊢ T ➡[h,n1] T1 →
∀T2. ⇧[1]T2 ≘ T → ∀n2,XT2. ❪G,L❫ ⊢ T2 ➡[h,n2] XT2 →
qed-.
fact cnv_cpm_conf_lpr_zeta_zeta_aux (h) (a) (G) (L) (V) (T):
- (∀G0,L0,T0. ❪G,L,+ⓓV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,+ⓓV.T❫ > ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
❪G,L❫ ⊢ +ⓓV.T ![h,a] →
∀T1. ⇧[1]T1 ≘ T → ∀T2. ⇧[1]T2 ≘ T →
∀n1,XT1. ❪G,L❫ ⊢ T1 ➡[h,n1] XT1 → ∀n2,XT2. ❪G,L❫ ⊢ T2 ➡[h,n2] XT2 →
qed-.
fact cnv_cpm_conf_lpr_appl_appl_aux (h) (a) (G) (L) (V) (T):
- (∀G0,L0,T0. ❪G,L,ⓐV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,ⓐV.T❫ > ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
❪G,L❫ ⊢ ⓐV.T ![h,a] →
∀V1. ❪G,L❫ ⊢ V ➡[h,0] V1 → ∀V2. ❪G,L❫ ⊢ V ➡[h,0] V2 →
∀n1,T1. ❪G,L❫ ⊢ T ➡[h,n1] T1 → ∀n2,T2. ❪G,L❫ ⊢ T ➡[h,n2] T2 →
qed-.
fact cnv_cpm_conf_lpr_appl_beta_aux (h) (a) (p) (G) (L) (V) (W) (T):
- (∀G0,L0,T0. ❪G,L,ⓐV.ⓛ[p]W.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,ⓐV.ⓛ[p]W.T❫ > ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
❪G,L❫ ⊢ ⓐV.ⓛ[p]W.T ![h,a] →
∀V1. ❪G,L❫ ⊢ V ➡[h,0] V1 → ∀V2. ❪G,L❫ ⊢ V ➡[h,0] V2 →
∀W2. ❪G,L❫ ⊢ W ➡[h,0] W2 →
qed-.
fact cnv_cpm_conf_lpr_appl_theta_aux (h) (a) (p) (G) (L) (V) (W) (T):
- (∀G0,L0,T0. ❪G,L,ⓐV.ⓓ[p]W.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,ⓐV.ⓓ[p]W.T❫ > ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
❪G,L❫ ⊢ ⓐV.ⓓ[p]W.T ![h,a] →
∀V1. ❪G,L❫ ⊢ V ➡[h,0] V1 → ∀V2. ❪G,L❫ ⊢ V ➡[h,0] V2 →
∀W2. ❪G,L❫ ⊢ W ➡[h,0] W2 →
qed-.
fact cnv_cpm_conf_lpr_beta_beta_aux (h) (a) (p) (G) (L) (V) (W) (T):
- (∀G0,L0,T0. ❪G,L,ⓐV.ⓛ[p]W.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,ⓐV.ⓛ[p]W.T❫ > ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
❪G,L❫ ⊢ ⓐV.ⓛ[p]W.T ![h,a] →
∀V1. ❪G,L❫ ⊢ V ➡[h,0] V1 → ∀V2. ❪G,L❫ ⊢ V ➡[h,0] V2 →
∀W1. ❪G,L❫ ⊢ W ➡[h,0] W1 → ∀W2. ❪G,L❫ ⊢ W ➡[h,0] W2 →
qed-.
fact cnv_cpm_conf_lpr_theta_theta_aux (h) (a) (p) (G) (L) (V) (W) (T):
- (∀G0,L0,T0. ❪G,L,ⓐV.ⓓ[p]W.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,ⓐV.ⓓ[p]W.T❫ > ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
❪G,L❫ ⊢ ⓐV.ⓓ[p]W.T ![h,a] →
∀V1. ❪G,L❫ ⊢ V ➡[h,0] V1 → ∀V2. ❪G,L❫ ⊢ V ➡[h,0] V2 →
∀W1. ❪G,L❫ ⊢ W ➡[h,0] W1 → ∀W2. ❪G,L❫ ⊢ W ➡[h,0] W2 →
qed-.
fact cnv_cpm_conf_lpr_cast_cast_aux (h) (a) (G) (L) (V) (T):
- (∀G0,L0,T0. ❪G,L,ⓝV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,ⓝV.T❫ > ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
❪G,L❫ ⊢ ⓝV.T ![h,a] →
∀n1,V1. ❪G,L❫ ⊢ V ➡[h,n1] V1 → ∀n2,V2. ❪G,L❫ ⊢ V ➡[h,n2] V2 →
∀T1. ❪G,L❫ ⊢ T ➡[h,n1] T1 → ∀T2. ❪G,L❫ ⊢ T ➡[h,n2] T2 →
qed-.
fact cnv_cpm_conf_lpr_cast_epsilon_aux (h) (a) (G) (L) (V) (T):
- (∀G0,L0,T0. ❪G,L,ⓝV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,ⓝV.T❫ > ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
❪G,L❫ ⊢ ⓝV.T ![h,a] →
∀n1,V1. ❪G,L❫ ⊢ V ➡[h,n1] V1 →
∀T1. ❪G,L❫ ⊢ T ➡[h,n1] T1 → ∀n2,T2. ❪G,L❫ ⊢ T ➡[h,n2] T2 →
qed-.
fact cnv_cpm_conf_lpr_cast_ee_aux (h) (a) (G) (L) (V) (T):
- (∀G0,L0,T0. ❪G,L,ⓝV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpm_trans_lpr h a G0 L0 T0) →
- (∀G0,L0,T0. ❪G,L,ⓝV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,ⓝV.T❫ > ❪G0,L0,T0❫ → IH_cnv_cpm_trans_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,ⓝV.T❫ > ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
❪G,L❫ ⊢ ⓝV.T ![h,a] →
∀n1,V1. ❪G,L❫ ⊢ V ➡[h,n1] V1 → ∀n2,V2. ❪G,L❫ ⊢ V ➡[h,n2] V2 →
∀T1. ❪G,L❫ ⊢ T ➡[h,n1] T1 →
elim (cnv_cpms_strip_lpr_sub … IH1 … HVX0 … HV02 … L0 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
elim (cnv_cpms_strip_lpr_sub … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2 width=1 by fqup_fpbg/ ]
-HV02 -HTX0 -HT01 <minus_O_n <minus_n_O #T #HT2 #HT1 #V #HV1 #HV2
-elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
+elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=5 by fqup_cpms_fwd_fpbg/ ]
-L0 -V0 -T0 -X0 #U #HVU #HTU
lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
lapply (cpms_trans … HT1 … HTU) -T <arith_l2 #H1
qed-.
fact cnv_cpm_conf_lpr_epsilon_epsilon_aux (h) (a) (G) (L) (V) (T):
- (∀G0,L0,T0. ❪G,L,ⓝV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,ⓝV.T❫ > ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
❪G,L❫ ⊢ ⓝV.T ![h,a] →
∀n1,T1. ❪G,L❫ ⊢ T ➡[h,n1] T1 → ∀n2,T2. ❪G,L❫ ⊢ T ➡[h,n2] T2 →
∀L1. ❪G,L❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L❫ ⊢ ➡[h,0] L2 →
qed-.
fact cnv_cpm_conf_lpr_epsilon_ee_aux (h) (a) (G) (L) (V) (T):
- (∀G0,L0,T0. ❪G,L,ⓝV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpm_trans_lpr h a G0 L0 T0) →
- (∀G0,L0,T0. ❪G,L,ⓝV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,ⓝV.T❫ > ❪G0,L0,T0❫ → IH_cnv_cpm_trans_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,ⓝV.T❫ > ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
❪G,L❫ ⊢ ⓝV.T ![h,a] →
∀n1,T1. ❪G,L❫ ⊢ T ➡[h,n1] T1 → ∀n2,V2. ❪G,L❫ ⊢ V ➡[h,n2] V2 →
∀L1. ❪G,L❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L❫ ⊢ ➡[h,0] L2 →
elim (cnv_cpms_strip_lpr_sub … IH1 … HVX0 … HV02 … L0 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
elim (cnv_cpms_strip_lpr_sub … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2 width=1 by fqup_fpbg/ ]
-HV02 -HTX0 -HT01 <minus_O_n <minus_n_O #T #HT2 #HT1 #V #HV1 #HV2
-elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
+elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=5 by fqup_cpms_fwd_fpbg/ ]
-L0 -V0 -T0 -X0 #U #HVU #HTU
lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
lapply (cpms_trans … HT1 … HTU) -T <arith_l2 #H1
qed-.
fact cnv_cpm_conf_lpr_ee_ee_aux (h) (a) (G) (L) (V) (T):
- (∀G0,L0,T0. ❪G,L,ⓝV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ (∀G0,L0,T0. ❪G,L,ⓝV.T❫ > ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
❪G,L❫ ⊢ ⓝV.T ![h,a] →
∀n1,V1. ❪G,L❫ ⊢ V ➡[h,n1] V1 → ∀n2,V2. ❪G,L❫ ⊢ V ➡[h,n2] V2 →
∀L1. ❪G,L❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L❫ ⊢ ➡[h,0] L2 →
fact cnv_cpm_conf_lpr_aux (h) (a):
∀G0,L0,T0.
- (∀G1,L1,T1. ❪G0,L0,T0❫ >[h] ❪G1,L1,T1❫ → IH_cnv_cpm_trans_lpr h a G1 L1 T1) →
- (∀G1,L1,T1. ❪G0,L0,T0❫ >[h] ❪G1,L1,T1❫ → IH_cnv_cpms_conf_lpr h a G1 L1 T1) →
+ (∀G1,L1,T1. ❪G0,L0,T0❫ > ❪G1,L1,T1❫ → IH_cnv_cpm_trans_lpr h a G1 L1 T1) →
+ (∀G1,L1,T1. ❪G0,L0,T0❫ > ❪G1,L1,T1❫ → IH_cnv_cpms_conf_lpr h a G1 L1 T1) →
∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_conf_lpr h a G1 L1 T1.
#h #a #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]]
[ #I #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct