proposition: Lemma satCongr P Q : (forall a b c d, P ((a,b),(c,d)) <-> Q ((a,b),(c,d))) -> sat P -> sat Q.
proof: Proof. intros H [H1 [H2 H3]]. split. 2:split. - unfold ax1 in *. intros a c. rewrite <- H. apply H1. - unfold ax2 in *. intros a b c d. rewrite <- H. split. * destruct (H2 a b c d) as [H2' _]. intros H4. destruct (H2' H4) as [b' [c' [d' H5]]]. exists b', c', d'. rewrite <- !H. apply H5. * destruct (H2 a b c d) as [_ H2']. intros [b' [c' [d' H4]]]. apply H2'. exists b',c',d'. rewrite !H. apply H4. - unfold ax3 in *. intros a c d. rewrite <- H. apply H3. Qed.
imports: Arith Lia List Undecidability.DiophantineConstraints(H10C)