proposition: Lemma is_var_of_clause_merge : forall v cl1 cl2, is_var_of_clause v (Elim.merge_clause cl1 cl2) <-> is_var_of_clause v (cl1 ++ cl2).
proof: Proof. unfold Elim.merge_clause. intros. destruct (Elim.split_clause cl1) as (cln1,clp1) eqn:SC1. destruct (Elim.split_clause cl2) as (cln2,clp2) eqn:SC2. rewrite! is_var_of_clause_app. apply is_var_of_clause_split with (v:=v) in SC1. apply is_var_of_clause_split with (v:=v) in SC2. rewrite is_var_of_clause_app in *. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause