proposition: Lemma check_annot_TRUE : forall hm, check_annot has_clause hm (Annot.mk_elt TRUE).
proof: Proof. constructor ; auto. apply wf_pset_empty. exact I. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause