proposition: Lemma check_annot_lhTT : forall m, wf m -> check_annot has_literal m lhTT.
proof: Proof. constructor. apply wf_pset_empty. apply wf_hTT; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause