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