proposition: Fact h10luc_vars_equiv l phi psy : (forall x, In x (h10luc_vars l) -> phi x = psy x) -> forall c, In c l -> ⟪c⟫ phi <-> ⟪c⟫ psy.
proof: Proof. intros H c Hc. apply h10uc_vars_equiv. intros x Hx; apply H, in_flat_map. exists c; auto. Qed.
imports: List Arith Undecidability.Shared.Libs.DLW.Utils(utils_decidable utils_nat) Undecidability.DiophantineConstraints(H10C)