(**************************************************************************)
include "basic_2/grammar/lpx_sn_lpx_sn.ma".
(**************************************************************************)
include "basic_2/grammar/lpx_sn_lpx_sn.ma".
include "basic_2/reduction/lpr_ldrop.ma".
(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
include "basic_2/reduction/lpr_ldrop.ma".
(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
elim (lift_total V 0 (i+1)) #T #HVT
lapply (cpr_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/
elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
elim (lift_total V 0 (i+1)) #T #HVT
lapply (cpr_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/
elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
elim (lift_total V 0 (i+1)) #T #HVT
lapply (cpr_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1
elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
elim (lift_total V 0 (i+1)) #T #HVT
lapply (cpr_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1
[ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
elim (cpr_inv_atom1 … H1) -H1
elim (cpr_inv_atom1 … H2) -H2
[ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
elim (cpr_inv_atom1 … H1) -H1
elim (cpr_inv_atom1 … H2) -H2