proposition: Lemma h10sqc_of_h10ucs_spec {c} : Forall (h10uc_sem φ') (h10sqc_to_h10ucs c) -> h10sqc_sem φ c.
proof: Proof. Proof using Hφ'. case: c => /=. - move=> x /Forall_cons_iff []. rewrite /= ?(proj1 v_spec) /φ. by lia. - move=> x y z. do 9 (move=> /Forall_cons_iff /and_comm []). rewrite /= ?(proj1 v_spec) ?(proj2 v_spec) /φ. by lia. - move=> x y /Forall_cons_iff [+] /Forall_cons_iff [+ _]. rewrite /= ?(proj1 v_spec) /φ. by lia. Qed.
imports: List Lia Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun