proposition: Lemma wf_app_conflict_clause : forall [hm l1 l2] (WFL1: Forall (has_literal hm) l1) (WFL2: Forall (has_literal hm) l2), Forall (has_literal hm) (l1 ++ l2).
proof: Proof. unfold generate_conflict_clause. intros. rewrite Forall_app. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause