proposition: Lemma is_mask_same: forall m p q, Key.is_mask m p -> Key.is_mask m q -> p = q.
proof: Proof. intros; unfold Key.is_mask in *; unfold K.is_mask in *. generalize (proj2 (H0 q) eq_refl); intros. eapply H; auto. Qed.
imports: Lia Cdcl.Coqlib