proposition: Fact h10uc_vars_equiv c phi psy : (forall x, In x (h10uc_vars c) -> phi x = psy x) -> ⟪c⟫ phi <-> ⟪c⟫ psy.
proof: Proof. destruct c as ((?,?),?); simpl; intros H; repeat rewrite H; tauto. Qed.
imports: List Arith Undecidability.Shared.Libs.DLW.Utils(utils_decidable utils_nat) Undecidability.DiophantineConstraints(H10C)