proposition: Lemma check_annot_lit : forall [hm f], has_form hm f -> check_annot has_literal hm (annot_lit f).
proof: Proof. unfold annot_lit. split ; auto. simpl. apply wf_pset_singleton ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause