proposition: Lemma wf_add_conclusion : forall [hm l1 l2 g] (WFL1: Forall (has_literal hm) l1) (WFL2: Forall (has_literal hm) l2) (HASG: has_oform hm g) , Forall (has_literal hm) (fst (add_conclusion g (l1,l2))) /\ Forall (has_literal hm) (snd (add_conclusion g (l1,l2))).
proof: Proof. unfold add_conclusion. destruct g ; auto. simpl. destruct (elt h) eqn:EQ; simpl; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause