proposition: Lemma ojoinA (U : unlifted) (x y z : U) : obind (ojoin x) (ojoin y z) = obind (@ojoin U^~ z) (ojoin x y).
proof: Proof. by case: U x y z=>T [ou oj ojC ojA]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype) pcm(options prelude) pcm(pcm morphism)