proposition: Lemma wf_normalise : forall cl cl', wf cl -> Elim.normalise cl = Some cl' -> wf cl'.
proof: Proof. intros. apply sublist_normalise in H0. eapply wf_sublist; eauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause