1 (* (C) 2014 Luca Bressan *)
8 mk_est n0 (λz,z'. z = z') ?.
9 % #x [ % | #y * % | #y #z #h * @h ]
12 definition en0_rect_Type0: ∀Q: edst en0. epi en0 Q ≝
13 λQ. 〈n0_rect_Type0 …, ?〉.
17 definition en0_rect_Type1: ∀Q: edcl (est_into_ecl en0). ePi … Q ≝
18 λQ. 〈n0_rect_Type1 …, ?〉.
22 definition edn0: ∀I: est. edst I ≝ λI. constant_edst I en0.