proposition: Lemma wf_resolve_all : forall lp ln (WF1 : Forall wf lp) (WF2 : Forall wf ln) , Forall wf (Elim.resolve_all lp ln).
proof: Proof. induction lp. - simpl. constructor. - simpl. intros. rewrite Forall_app. split; auto. assert (Forall wf (map (Elim.merge_clause a) ln)). inv WF1. induction ln. constructor. simpl. constructor. apply wf_merge_clause;auto. inv WF2;auto. apply IHln. inv WF2;auto. induction ((map (Elim.merge_clause a) ln)). + simpl. constructor. + simpl. inv H. destruct (Elim.normalise a0) eqn:N. constructor. eapply wf_normalise;eauto. apply IHl;auto. apply IHl;auto. + apply IHlp;auto. inv WF1;auto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause