proposition: Lemma v_spec : φ' (v 0) = 0 /\ φ' (v 1) = 1.
proof: Proof. Proof using Hφ'. move: (Hφ'). rewrite -Forall_forall /ucs Forall_app /v012. move=> [/Forall_cons_iff [+]] /Forall_cons_iff [+] /Forall_cons_iff [+] _ _ => /=. by nia. Qed.
imports: List Lia Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun