proposition: Lemma poly_of_formula_sound : forall fl fr var, poly_of_formula fl = 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. rewrite Heq; reflexivity. Qed.
imports: Bool DecidableClass Algebra Ring PArith Lia