proposition: Lemma lim_dappE A (D : A -> cpo) (s : chain (dfunCPO D)) (x : A) : lim s x = lim (dapp_chain s x).
proof: Proof. by []. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)