proposition: Lemma check_annot_set : forall {A B: Type} (P: hmap -> A -> Prop) (Q: hmap -> B -> Prop) m v v' (C1 : check_annot P m v) (HAS : Q m v') , check_annot Q m (Annot.set v v').
proof: Proof. intros. destruct C1. constructor ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause