proposition: Lemma dfun_limM (s : chain tp) x : (forall y, y \In s -> y <== x) -> dfun_lim s <== x.
proof: Proof. by move=>H1 t; apply: limM=>y [f][->] H2; apply: H1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)