proposition: Lemma satEquiv P Q : sat P -> satw Q -> forall a b c d, P ((a,b),(c,d)) -> Q ((a,b),(c,d)).
proof: Proof. intros [HP1 [HP2 HP3]] [HQ1 HQ2] a b c d. induction b as [|b' IH] in a,c,d|-*. * apply satEquiv0; firstorder. * destruct (HP2 a (S b') c d) as [HP21 HP22]. pose proof (HQ2 a (S b') c d) as HQ22. intros H. - apply HQ22. destruct HP21 as [b'' [c' [d' [H1 [H2 [H3 H4]]]]]]. + split; easy. + exists b'', c', d'. unfold ax1 in HP1. rewrite HP1 in H3. assert (b'' = b') as -> by lia. unfold ax1 in HQ1. rewrite !HQ1. rewrite <- !HP1. rewrite <- HP1 in H3. split. 2:split. 3:tauto. all: apply IH; easy. Qed.
imports: Arith Lia List Undecidability.DiophantineConstraints(H10C)