/3 width=1 by or3_intro0, conj/
] *
#cV #L #W #W2 #HKL #HW2 #HWV2 #H destruct
- lapply (lifts_trans … HWV2 … HVT2 ??) -V2 [3,6: |*: // ] #H
-(* lapply (lifts_uni … H) -H #H *) (**)
+ lapply (lifts_trans … HWV2 … HVT2 (𝐔❨↑↑i❩) ?) -V2 [1,3: // ] #H (**) (* explicit rtmap *)
/4 width=8 by drops_drop, ex4_4_intro, or3_intro2, or3_intro1/
]
qed-.