proposition: Lemma h10c_to_h10sqcs_spec {c} : h10c_sem c φ -> Forall (h10sqc_sem φ') (h10c_to_h10sqcs c).
proof: Proof. case: c => /=. - move=> x ?. constructor; last done. by rewrite /= /ζ /φ' Cantor.cancel_of_to. - move=> x y z ?. constructor; last done. by rewrite /= /ζ /φ' ?Cantor.cancel_of_to. - move=> x y z ?. (do ? constructor); rewrite /= /ζ /φ' ?Cantor.cancel_of_to /= ?Cantor.cancel_of_to; by nia. Qed.
imports: List Lia Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun