matita/matita/contribs/mf/empty.ma

   1 (* (C) 2014 Luca Bressan *)
   2
   3 include "model.ma".
   4 include "pisigma.ma".
   5 include "pisigma2.ma".
   6
   7 definition en0: est ≝
   8  mk_est n0 (λz,z'. z = z') ?.
   9  % #x [ % | #y * % | #y #z #h * @h ]
  10 qed.
  11
  12 definition en0_rect_Type0: ∀Q: edst en0. epi en0 Q ≝
  13  λQ. 〈n0_rect_Type0 …, ?〉.
  14  @(n0_rect_CProp0).
  15 qed.
  16
  17 definition en0_rect_Type1: ∀Q: edcl (est_into_ecl en0). ePi … Q ≝
  18  λQ. 〈n0_rect_Type1 …, ?〉.
  19  @(n0_rect_CProp1).
  20 qed.
  21
  22 definition edn0: ∀I: est. edst I ≝ λI. constant_edst I en0.
  23