(* Basic_2A1: includes: lpx_sn_deliftable_dropable *)
lemma lexs_deliftable_dropable: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_sn RP →
(* Basic_2A1: includes: lpx_sn_deliftable_dropable *)
lemma lexs_deliftable_dropable: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_sn RP →