proposition: Lemma cnv_ext `{laws} `{CNV ≪ l} n m (x: X n m): x ≦ x⋅x°⋅x.
proof: Proof. destruct cnv_ext_; trivial. transitivity ((x⋅1) ∩ x). rewrite dotx1. lattice. rewrite capdotx, <-dotA. apply dot_leq; lattice. Qed.
imports: lattice