| #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct
lapply (cprs_strap1 … HV10 … HV02) -V0 #HV12
lapply (lsubr_cpr_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2
- /5 width=5 by cprs_bind, cprs_flat_dx, cpr_cprs, lsubr_abst, ex2_3_intro, or3_intro1/
+ /5 width=5 by cprs_bind, cprs_flat_dx, cpr_cprs, lsubr_beta, ex2_3_intro, or3_intro1/
| #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct
/5 width=10 by cprs_flat_sn, cprs_bind_dx, cprs_strap1, ex4_5_intro, or3_intro2/
]
#G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2
[ /2 width=3 by/
| #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
- elim (lpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+ elim (lpr_drop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
elim (lpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
/4 width=6 by cprs_strap2, cprs_delta/
|3,7: /4 width=1 by lpr_pair, cprs_bind, cprs_beta/
-|4,6: /3 width=1 by cprs_flat, cprs_tau/
+|4,6: /3 width=1 by cprs_flat, cprs_eps/
|5,8: /4 width=3 by lpr_pair, cprs_zeta, cprs_theta, cprs_strap1/
]
qed-.