proposition: Lemma sat_satw P : sat P -> satw P.
proof: Proof. intros [H1 [H2 H3]]. split. * easy. * intros a b c d H. destruct (H2 a b c d) as [_ H2R]. now apply H2R. Qed.
imports: Arith Lia List Undecidability.DiophantineConstraints(H10C)