proposition: Lemma wf_elim : forall x cls, Forall wf cls -> Forall wf (Elim.elim x cls).
proof: Proof. unfold Elim.elim. intros. destruct (Elim.split_polarity x cls) as ((lp,ln),lo) eqn:SP. apply wf_split_polarity in SP; auto. rewrite Forall_app. split ; try tauto. apply wf_resolve_all;tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause