proposition: Lemma eval_mk_impl : forall l r, eval_formula (LIMPL l r) <-> eval_formula (mk_impl l r).
proof: Proof. unfold mk_impl. intros. destruct (elt r) eqn:EQ; try tauto. rewrite eval_formula_rew. symmetry. rewrite eval_formula_rew. rewrite<- !eval_impl_list_eq. rewrite! eval_and_list_eq. rewrite eval_and_list_rev_append. rewrite EQ. simpl. rewrite <- eval_impl_list_eq. rewrite eval_and_list_eq. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause