matita/matita/contribs/mf/interface.ma

   1 (* (C) 2014 Luca Bressan *)
   2
   3 include "model.ma".
   4
   5 include "pisigma2.ma".
   6 include "power_one.ma".
   7 include "power.ma".
   8
   9 include "pisigma.ma".
  10 include "empty.ma".
  11 include "singleton.ma".
  12 include "list.ma".
  13 include "plus.ma".
  14 include "de.ma".
  15
  16 definition eFalsum: eprop ≝ Falsum.
  17 definition eId: ∀B: ecl. Sup B → Sup B → eprop ≝ Eq.
  18 definition eImplies: eprop → eprop → eprop ≝ Implies.
  19 definition eConj: eprop → eprop → eprop ≝ Conj.
  20 definition eDisj: eprop → eprop → eprop ≝ Disj.
  21
  22 definition efalsum: eprops ≝ falsum.
  23 definition eid: ∀B: est. sup B → sup B → eprops ≝ eq.
  24 definition eimplies: eprops → eprops → eprops ≝ implies.
  25 definition econj: eprops → eprops → eprops ≝ conj.
  26 definition edisj: eprops → eprops → eprops ≝ disj.
  27