proposition: Lemma reduce_poly_of_formula_sound : forall fl fr var, reduce (poly_of_formula fl) = reduce (poly_of_formula fr) -> formula_eval var fl = formula_eval var fr.
proof: Proof. intros fl fr var Heq. repeat rewrite <- poly_of_formula_eval_compat. destruct (poly_of_formula_valid_compat fl) as [nl Hl]. destruct (poly_of_formula_valid_compat fr) as [nr Hr]. rewrite <- (reduce_eval_compat nl (poly_of_formula fl)); auto. rewrite <- (reduce_eval_compat nr (poly_of_formula fr)); auto. rewrite Heq; reflexivity. Qed.
imports: Bool DecidableClass Algebra Ring PArith Lia