- elim (cpg_inv_flat1 … H2) -H2 *
- [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
- elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 //
- elim (IH … HT12 … HLK … HTU1) -IH -HT12 -HLK -HTU1 //
- /3 width=5 by cpg_flat, lifts_flat, ex2_intro/
- | #cT #HT12 #H1 #H2 destruct
- elim (IH … HT12 … HLK … HTU1) -IH -HT12 -HLK -HTU1 //
- /3 width=3 by cpg_eps, ex2_intro/
- | #cV #HV12 #H1 #H2 destruct
- elim (IH … HV12 … HLK … HVW1) -IH -HV12 -HLK -HVW1 //
- /3 width=3 by cpg_ee, ex2_intro/
- | #cV #cY #cT #a #V2 #Y1 #Y2 #T0 #T2 #HV12 #HY12 #HT12 #H1 #H2 #H3 #H4 destruct
- elim (lifts_inv_bind1 … HTU1) -HTU1 #Z1 #U0 #HYZ1 #HTU1 #H destruct
- elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 //
- elim (IH … HY12 … HLK … HYZ1) -HY12 //
- elim (IH … HT12 … HTU1) -IH -HT12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
- /4 width=7 by cpg_beta, lifts_bind, lifts_flat, ex2_intro/
- | #cV #cY #cT #a #V2 #V20 #Y1 #Y2 #T0 #T2 #HV12 #HV20 #HY12 #HT12 #H1 #H2 #H3 #H4 destruct
- elim (lifts_inv_bind1 … HTU1) -HTU1 #Z1 #U0 #HYZ1 #HTU1 #H destruct
- elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 // #W2 #HVW2 #HW12
- elim (IH … HY12 … HLK … HYZ1) -HY12 //
- elim (IH … HT12 … HTU1) -IH -HT12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
- elim (lifts_total W2 (𝐔❴1❵)) #W20 #HW20
- lapply (lifts_trans … HVW2 … HW20 ??) -HVW2 [3: |*: // ] #H
- lapply (lifts_conf … HV20 … H (↑f) ?) -V2 /2 width=3 by after_uni_one_sn/
- /4 width=9 by cpg_theta, lifts_bind, lifts_flat, ex2_intro/
+ [ elim (cpg_inv_appl1 … H2) -H2 *
+ [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
+ elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 //
+ elim (IH … HT12 … HLK … HTU1) -IH -HT12 -HLK -HTU1 //
+ /3 width=5 by cpg_appl, lifts_flat, ex2_intro/
+ | #cV #cY #cT #a #V2 #Y1 #Y2 #T0 #T2 #HV12 #HY12 #HT12 #H1 #H2 #H3 destruct
+ elim (lifts_inv_bind1 … HTU1) -HTU1 #Z1 #U0 #HYZ1 #HTU1 #H destruct
+ elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 //
+ elim (IH … HY12 … HLK … HYZ1) -HY12 //
+ elim (IH … HT12 … HTU1) -IH -HT12 -HTU1 [ |*: /3 width=3 by drops_skip, ext2_pair/ ]
+ /4 width=7 by cpg_beta, lifts_bind, lifts_flat, ex2_intro/
+ | #cV #cY #cT #a #V2 #V20 #Y1 #Y2 #T0 #T2 #HV12 #HV20 #HY12 #HT12 #H1 #H2 #H3 destruct
+ elim (lifts_inv_bind1 … HTU1) -HTU1 #Z1 #U0 #HYZ1 #HTU1 #H destruct
+ elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 // #W2 #HVW2 #HW12
+ elim (IH … HY12 … HLK … HYZ1) -HY12 //
+ elim (IH … HT12 … HTU1) -IH -HT12 -HTU1 [ |*: /3 width=3 by drops_skip, ext2_pair/ ]
+ elim (lifts_total W2 (𝐔❴1❵)) #W20 #HW20
+ lapply (lifts_trans … HVW2 … HW20 ??) -HVW2 [3: |*: // ] #H
+ lapply (lifts_conf … HV20 … H (⫯f) ?) -V2 /2 width=3 by after_uni_one_sn/
+ /4 width=9 by cpg_theta, lifts_bind, lifts_flat, ex2_intro/
+ ]
+ | elim (cpg_inv_cast1 … H2) -H2 *
+ [ #cV #cT #V2 #T2 #HV12 #HT12 #HcVT #H1 #H2 destruct
+ elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 //
+ elim (IH … HT12 … HLK … HTU1) -IH -HT12 -HLK -HTU1 //
+ /3 width=5 by cpg_cast, lifts_flat, ex2_intro/
+ | #cT #HT12 #H destruct
+ elim (IH … HT12 … HLK … HTU1) -IH -HT12 -HLK -HTU1 //
+ /3 width=3 by cpg_eps, ex2_intro/
+ | #cV #HV12 #H destruct
+ elim (IH … HV12 … HLK … HVW1) -IH -HV12 -HLK -HVW1 //
+ /3 width=3 by cpg_ee, ex2_intro/
+ ]