proposition: Lemma mx_map_blk {X Y l} {HY: lattice.laws l Y} (f: X -> Y) n1 n2 m1 m2 a b c d: mx_map f (@blk_mx _ n1 n2 m1 m2 a b c d) ≡ blk_mx (mx_map f a) (mx_map f b) (mx_map f c) (mx_map f d).
proof: Proof. intros i j. unfold mx_map, blk_mx, col_mx, row_mx. case split; case split; reflexivity. Qed.
imports: kleene normalisation ordinal sups matrix