proposition: Lemma is_var_of_clause_split : forall v cl cln1 clp1, Elim.split_clause cl = (cln1, clp1) -> is_var_of_clause v cl <-> is_var_of_clause v (cln1 ++clp1).
proof: Proof. induction cl;simpl;intros. - inv H. simpl. tauto. - destruct a. inv H. simpl. rewrite! is_var_of_clause_cons. tauto. destruct (Elim.split_clause cl) as (cln2,clp2) eqn:SC1. inv H. rewrite! is_var_of_clause_app. rewrite! is_var_of_clause_cons. rewrite IHcl by reflexivity. rewrite is_var_of_clause_app. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause