proposition: Lemma mx_map_fun {X Y: lattice.ops} {l} {HY: lattice.laws l Y} n m f z g: g bot ≡ bot -> mx_map g (@mx_fun X n m f z) ≡ @mx_fun Y n m f (g z).
proof: Proof. intros Hg i j. unfold mx_map, mx_fun. now case eqb_ord. Qed.
imports: kleene normalisation ordinal sups matrix