fact: Definition ax2w (P : (nat*nat)*(nat*nat) -> Prop) := forall a b c d , (exists b' c' d', P ((a,b'),(c',d')) /\ P ((d',b'),(d,d')) /\ P ((b',0),(b,0)) /\ P ((c',0),(c,0))) -> (P ((a,b),(c,d))).
imports: Arith Lia List Undecidability.DiophantineConstraints(H10C)