proposition: Lemma merge_clause_correct : forall env v cl cl', wf cl -> wf cl' -> eval_clause env (cons_lit (POS v) cl) -> eval_clause env (cons_lit (NEG v) cl') -> eval_clause env (Elim.merge_clause cl cl').
proof: Proof. intros. unfold wf in *. destruct H as (l1 & l2 & EQ). destruct H0 as (l1' & l2' & EQ'). subst. unfold Elim.merge_clause. rewrite! split_clause_wf. rewrite cons_lit_NEG_wf in H2. rewrite cons_lit_POS_wf in H1. simpl in H2. repeat rewrite eval_clause_wf in *. unfold eval_lit in H2. simpl in H2. intros. rewrite <- map_app. rewrite eval_clause_or. rewrite eval_or_app. rewrite eval_clause_or in *. simpl in H1. unfold eval_lit in H1. simpl in H1. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause