proposition: Lemma mem_of_row n i (u: rmx 1 n): is_01_mx u -> forall j, ofbool (set.mem (of_row u) j) ≡ u i j.
proof: Proof. intros Hu j. unfold of_row. rewrite set.mem_of_fun. symmetry. setoid_rewrite ord0_unique. apply expand_01, Hu. Qed.
imports: monoid regex lset boolean sups matrix_ext normalisation