- lapply (lift_inv_lref2_ge … H … Hdei) -H #H destruct -T1;
- lapply (ldrop_conf_ge … HLK … HLKV ?) -HLK HLKV L // #HKV
- elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW; [4: // | 2,3: normalize /2/ ] -Hdei >arith_e2 // #V0 #HV10 #HV02
- @ex2_1_intro
- [2: @tps_subst [3: /2/ |5,6: // |1,2: skip |4: @arith5 // ]
- |1: skip
- | //
- ] (**) (* explicitc constructors *)
+ lapply (lift_inv_lref2_ge … H … Hdei) -H #H destruct
+ lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV
+ elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |2,3: normalize /2 width=1/ ] -Hdei >arith_e2 // #V0 #HV10 #HV02
+ @ex2_1_intro /3 width=4/ (**) (* explicitc constructors *)