(* Basic_1: includes: pr3_gen_lift *)
lemma cpms_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn … lifts (λL. cpms h G L n).
/3 width=6 by d2_deliftable_sn_ltc, cpm_inv_lifts_sn/ qed-.
(* Basic_1: includes: pr3_gen_lift *)
lemma cpms_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn … lifts (λL. cpms h G L n).
/3 width=6 by d2_deliftable_sn_ltc, cpm_inv_lifts_sn/ qed-.