proposition: Lemma is_var_of_clause_app : forall v cl1 cl2, is_var_of_clause v (cl1++cl2) <-> is_var_of_clause v cl1 \/ is_var_of_clause v cl2.
proof: Proof. induction cl1;simpl;intros. - rewrite is_var_of_clause_nil. tauto. - rewrite! is_var_of_clause_cons. rewrite! IHcl1. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause