proposition: Lemma bmx_str_str n (M: bmx n n): M^* ≡ bmx_str M.
proof: Proof. induction n as [|n IHn]. intro i. elim (ord_0_empty i). change (M^*) with (mx_str _ _ _ M). simpl mx_str. simpl bmx_str. unfold mx_str_build. ra_fold (mx_ops bool_ops bool_tt). rewrite bmx_top_1. now rewrite IHn, dot1x, dotx1. Qed.
imports: kleene boolean sups matrix