proposition: Lemma h10c_of_h10sqcs_spec {c} : Forall (h10sqc_sem φ') (h10c_to_h10sqcs c) -> h10c_sem c φ.
proof: Proof. case: c => /=. - by move=> x /Forall_cons_iff []. - by move=> x y z /Forall_cons_iff []. - move=> x y z. do 7 (move=> /Forall_cons_iff /and_comm []). rewrite /= /φ. by nia. Qed.
imports: List Lia Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun