proposition: Lemma base_equiv a c d : h10upc_sem_direct ((a,0),(c,d)) <-> h10upc_ind a 0 c d.
proof: Proof. split. * intros [H1 H2]. assert (d=0) as -> by lia. assert (c = S a) as -> by lia. apply base. * intros H. inversion H as [a' H1|a' b' c' d' b'' c'' d'' H1 H2 H3 H4 H5]. - cbn. lia. - exfalso. now eapply h10upc_ind_not_less_0 with b''. Qed.
imports: Arith Lia List Undecidability.DiophantineConstraints(H10C)