elim (lift_total T l k)
/3 width=15 by cprs_lift, da_lift, lstas_lift, ex4_2_intro/
qed.
lemma scpds_inv_lift1: ∀h,o,G,d. d_deliftable_sn (scpds h o d G).
elim (lift_total T l k)
/3 width=15 by cprs_lift, da_lift, lstas_lift, ex4_2_intro/
qed.
lemma scpds_inv_lift1: ∀h,o,G,d. d_deliftable_sn (scpds h o d G).