proposition: Lemma h10_equiv a b c d : h10upc_sem_direct ((a,b),(c,d)) <-> h10upc_ind a b c d.
proof: Proof. induction b as [|b IH] in a,c,d|-*. - apply base_equiv. - symmetry. split. * intros H. inversion H; subst. rewrite <- base_equiv in H2, H3. cbn in H2,H3. assert (b' = b) as -> by lia. assert (S c' = c) as <- by lia. rewrite <- IH in H0,H1. cbn in H0,H1. cbn. lia. * intros [H1 H2]. eapply step with b (c-1) (d-b-1). + rewrite <- IH. cbn; lia. + rewrite <- IH. cbn; lia. + rewrite <- base_equiv. cbn; lia. + rewrite <- base_equiv. cbn; lia. Qed.
imports: Arith Lia List Undecidability.DiophantineConstraints(H10C)