proposition: Lemma ounitL (U : unlifted) (x : U) : ojoin ounit x = Some x.
proof: Proof. by case: U x=>T [ou oj ojC ojA ojL]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype) pcm(options prelude) pcm(pcm morphism)