1 (* (C) 2014 Luca Bressan *)
7 mk_est n1 (λz,z'. z = z') ?.
8 % #x [ % | #y * % | #y #z * * % ]
11 definition estar: en1 ≝ ⋆.
13 definition en1_rect_Type0: ∀Q: edst en1. eto (Q estar) (epi en1 Q).
15 [ #h @(〈n1_rect_Type0 (λw. Q w) h, ?〉)
17 @(rewrite_l … h (λz. (subst … d z) ≃ z) … (n1_rect_Type0 … h estar) (reflexivity …))
18 @tra [ @(h∘(ı…)) | @not_dep | @pres_id ]
23 definition edn1: ∀I: est. edst I ≝ λI. constant_edst I en1.