proposition: Lemma eval_formula_rew : forall f, eval_formula f = match f with | LAT a => eval_atom a | LOP o l => eval_op_list (fun f => eval_formula f.(elt)) o l | LIMPL l r => eval_impl_list (fun f => eval_formula f.(elt)) l (eval_formula r.(elt)) end.
proof: Proof. destruct f; reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause