proposition: Lemma nonempty_cod `{laws} `{TOP ≪ l} n m {x: X n m} {Hx: is_nonempty x}: is_nonempty' m.
proof: Proof. intros i j. rewrite nonempty. rewrite (leq_xt (top' i _⋅x)). ra. Qed.
imports: common lattice monoid kleene normalisation rewriting