proposition: Lemma mask_inj (T : eqType) (m1 m2 : bitseq) (s : seq T) : uniq s -> size m1 == size s -> size m2 == size s -> mask m1 s =i mask m2 s -> m1 == m2.
proof: Proof. elim: s m1 m2 => [m1 m2|a s IHs [|b1 m1] [|b2 m2] // U S1 S2 E]. - by rewrite /= !size_eq0 => _ /eqP-> /eqP->. - rewrite /= in U. move: U => /andP[U1 U2]. have mask_s : a \in mask _ s = false. move => b. apply: contraNF U1. exact: mem_mask. move: (E a). rewrite !mem_mask_cons !eqxx !andbT !mask_s !orbF => b12. rewrite eqseq_cons b12 eqxx IHs // => b. move: (E b). rewrite !mem_mask_cons. case: (boolP (b == a)) => [/eqP->|_]; by rewrite ?mask_s // ?andbF. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)