1 (* (C) 2014 Luca Bressan *)
6 include "power_one.ma".
11 include "singleton.ma".
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.
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.