proposition: Lemma is_mask_same': forall [m m' p], is_mask m p -> is_mask m' p -> m = m'.
proof: Proof. intros; eapply testbit_spec; intros. destruct (Nat.eq_dec p n). - subst p. rewrite (proj2 (H _) eq_refl). rewrite (proj2 (H0 _) eq_refl). reflexivity. - case_eq (testbit m n); intros. + elim n0. eapply (proj1 (H _) H1). + case_eq (testbit m' n); intros; auto. elim n0. eapply (proj1 (H0 _) H2). Qed.
imports: List Bool ZArith Lia