proposition: Lemma Exercise2_7B1 u: inc u closures -> cofinal r (fixpoints u).
proof: Proof. move /Zo_P => [/functionsP [ff sf tf] [pa pb pc]]. split; first by move => t /Zo_P[]; rewrite sf. move => x xsr; exists (Vf u x); last by apply: pb. apply/Zo_P; split; [ rewrite sf;Wtac; ue| by apply: pc]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)