proposition: Lemma forall_units_empty : forall P m , forall_units P m (IntMap.empty (Annot.t bool)).
proof: Proof. unfold forall_units. intros. unfold units_has_literal in H. destruct H. rewrite empty_o in H. congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause