proposition: Fact pm_lift_ext m n r1 r2 : @pm_ext_eq m n r1 r2 -> pm_ext_eq (pm_lift r1) (pm_lift r2).
proof: Proof. intros H12 p; unfold pm_lift. invert pos p; simpl; auto. f_equal; apply H12. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils)