proposition: Lemma check_annot_hyp : forall [m l] (HL: has_literal m l), check_annot has_literal m (annot_hyp l).
proof: Proof. unfold annot_hyp. intros. constructor ;auto. simpl. constructor. repeat constructor. intros. unfold LitSet.mem in H. simpl in H. exists (form_of_literal l). split ; auto. apply has_form_of_literal; auto. replace i with (id_of_literal l) by lia. reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause