(* *)
(**************************************************************************)
-include "ground_2/xoa/ex_5_5.ma".
+include "ground/xoa/ex_5_5.ma".
include "static_2/relocation/drops_drops.ma".
include "static_2/s_computation/fqup_weight.ma".
include "static_2/s_computation/fqup_drops.ma".
/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-.