proposition: Lemma split_clause_wf : forall l1 l2, Elim.split_clause (map NEG l1 ++ map POS l2) = (map NEG l1 , map POS l2).
proof: Proof. induction l1;simpl. - destruct l2 ; reflexivity. - intros. rewrite IHl1. reflexivity. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause