-inductive exT2 (A:Type) (P,Q:A→CProp) : CProp ≝
- ex_introT2: ∀w:A. P w → Q w → exT2 A P Q.
-
-record powerset (A: Type) : Type ≝ { char: A → CProp }.
-
-notation "hvbox(2 \sup A)" non associative with precedence 45
-for @{ 'powerset $A }.
-
-interpretation "powerset" 'powerset A = (powerset A).
-
-definition mem ≝ λA.λS:2 \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
-
-notation "hvbox(a break ∈ b)" non associative with precedence 45
-for @{ 'mem $a $b }.
-
-interpretation "mem" 'mem a S = (mem _ S a).
-
-record axiom_set : Type ≝
- { A:> Type;
- i: A → Type;
- C: ∀a:A. i a → 2 \sup A
- }.
-
-inductive for_all (A: axiom_set) (U,V: 2 \sup A) (covers: A → CProp) : CProp ≝