proposition: Lemma eqRelSat : sat h10upc_sem_direct.
proof: Proof. split. 2:split. - intros a c. cbn. lia. - intros a. intros. split. * intros [H1 [H2 H3]]. destruct b as [|b']. 1:easy. exists b', (c-1), (d-b'-1). repeat split. all: lia. * intros [b' [c' [d' [H1 [H2 [H3 H4]]]]]]. cbn in H1,H2,H3,H4. cbn; lia. - intros a c d. cbn. lia. Qed.
imports: Arith Lia List Undecidability.DiophantineConstraints(H10C)