proposition: Lemma satEquiv0 P Q : sat P -> satw Q -> forall a c d, P ((a,0),(c,d)) -> Q ((a,0),(c,d)).
proof: Proof. intros [HP1 [HP2 HP3]] [HQ1 HQ2] a c d. intros H. * pose proof (HP3 a c d H) as k. rewrite k in *. rewrite (HP1 a c) in H. rewrite (HQ1 a c). easy. Qed.
imports: Arith Lia List Undecidability.DiophantineConstraints(H10C)