fact: Fixpoint formula_eval var f := match f with | formula_var x => list_nth x var false | formula_btm => false | formula_top => true | formula_cnj fl fr => (formula_eval var fl) && (formula_eval var fr) | formula_dsj fl fr => (formula_eval var fl) || (formula_eval var fr) | formula_neg f => negb (formula_eval var f) | formula_xor fl fr => xorb (formula_eval var fl) (formula_eval var fr) | formula_ifb fc fl fr => if formula_eval var fc then formula_eval var fl else formula_eval var fr end.
imports: Bool DecidableClass Algebra Ring PArith Lia