- [ @tps_conf_subst_subst_lt /width=19/
- | -HVW1; destruct -i2;
- lapply (transitive_le ? ? (i1 + 1) Hdi2 ?) -Hdi2 // #Hdi2
- lapply (drop_mono … HLK1 … HLK2) -HLK1 Hdi1 Hi1de #H destruct -V1 K1;
- elim (IHVW1 … HVW2) -IHVW1 HVW2 #W #HW1 #HW2
- lapply (drop_fwd_drop2 … HLK2) -HLK2 #HLK2
- elim (lift_total W 0 (i1 + 1)) #T #HWT
- lapply (tps_lift_ge … HW1 … HLK2 HWT1 HWT ?) -HW1 HWT1 //
- lapply (tps_lift_ge … HW2 … HLK2 HWT2 HWT ?) -HW2 HWT2 HLK2 HWT // normalize #HT2 #HT1
- lapply (tps_weak … HT1 d e ? ?) -HT1 [ >arith_i2 // | // ]
- lapply (tps_weak … HT2 d e ? ?) -HT2 [ >arith_i2 // | // ]
- /2/
- | @ex2_1_comm @tps_conf_subst_subst_lt /width=19/
+ [ @tps_conf_subst_subst_lt /width=15/
+ | -Hdi2 Hi2de; destruct -i2;
+ lapply (drop_mono … HLK1 … HLK2) -HLK1 #H destruct -V1 K1
+ >(lift_mono … HVT1 … HVT2) -HVT1 /2/
+ | @ex2_1_comm @tps_conf_subst_subst_lt /width=15/