proposition: Lemma is_mask_same: forall {m p q}, is_mask m p -> is_mask m q -> p = q.
proof: Proof. intros; unfold is_mask in *; unfold is_mask in *. generalize (proj2 (H0 q) eq_refl); intros. eapply H; auto. Qed.
imports: List Bool ZArith Lia