+inductive Or (A,B:CProp) : CProp ≝
+ | or_intro_l: A → Or A B
+ | or_intro_r: B → Or A B.
+
+interpretation "constructive or" 'or x y = (Or x y).
+
+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).
+
+notation < "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i}. $p)}.
+
+interpretation "subset construction" 'subset \eta.x = (mk_powerset _ x).
+
+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).
+
+definition overlaps ≝ λA:Type.λU,V:2 \sup A.exT2 ? (λa:A. a ∈ U) (λa.a ∈ V).
+
+notation "hvbox(a break ≬ b)" non associative with precedence 45
+for @{ 'overlaps $a $b }. (* \between *)
+
+interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
+
+definition subseteq ≝ λA:Type.λU,V:2 \sup A.∀a:A. a ∈ U → a ∈ V.
+
+notation "hvbox(a break ⊆ b)" non associative with precedence 45
+for @{ 'subseteq $a $b }. (* \subseteq *)
+
+interpretation "subseteq" 'subseteq U V = (subseteq _ U V).
+
+definition intersects ≝ λA:Type.λU,V:2 \sup A.{a | a ∈ U ∧ a ∈ V}.
+
+notation "hvbox(a break ∩ b)" non associative with precedence 55
+for @{ 'intersects $a $b }. (* \cap *)
+
+interpretation "intersects" 'intersects U V = (intersects _ U V).
+
+definition union ≝ λA:Type.λU,V:2 \sup A.{a | a ∈ U ∨ a ∈ V}.
+
+notation "hvbox(a break ∪ b)" non associative with precedence 55
+for @{ 'union $a $b }. (* \cup *)
+
+interpretation "union" 'union U V = (union _ U V).
+
+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 ≝
+ iter: (∀a:A.a ∈ V → covers a) → for_all A U V covers.
+
+inductive covers (A: axiom_set) (U: 2 \sup A) : A → CProp ≝
+ refl: ∀a:A. a ∈ U → covers A U a
+ | infinity: ∀a:A. ∀j: i ? a. for_all A U (C ? a j) (covers A U) → covers A U a.
+
+notation "hvbox(a break ◃ b)" non associative with precedence 45
+for @{ 'covers $a $b }. (* a \ltri b *)
+
+interpretation "coversl" 'covers A U = (for_all _ U A (covers _ U)).
+interpretation "covers" 'covers a U = (covers _ U a).
+
+definition covers_elim ≝
+ λA:axiom_set.λU: 2 \sup A.λP:2 \sup A.
+ λH1:∀a:A. a ∈ U → a ∈ P.
+ λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → C ? a j ⊆ P → a ∈ P.
+ let rec aux (a:A) (p:a ◃ U) on p : a ∈ P ≝
+ match p return λaa.λ_:aa ◃ U.aa ∈ P with
+ [ refl a q ⇒ H1 a q
+ | infinity a j q ⇒
+ H2 a j q
+ match q return λ_:(C ? a j) ◃ U. C ? a j ⊆ P with
+ [ iter f ⇒ λb.λr. aux b (f b r) ]]
+ in
+ aux.
+
+inductive ex_such (A : axiom_set) (U,V : 2 \sup A) (fish: A → CProp) : CProp ≝
+ found : ∀a. a ∈ V → fish a → ex_such A U V fish.
+
+coinductive fish (A:axiom_set) (U: 2 \sup A) : A → CProp ≝
+ mk_fish: ∀a:A. a ∈ U → (∀j: i ? a. ex_such A U (C ? a j) (fish A U)) → fish A U a.
+
+notation "hvbox(a break ⋉ b)" non associative with precedence 45
+for @{ 'fish $a $b }. (* a \ltimes b *)
+
+interpretation "fishl" 'fish A U = (ex_such _ U A (fish _ U)).
+interpretation "fish" 'fish a U = (fish _ U a).
+
+let corec fish_rec (A:axiom_set) (U: 2 \sup A)
+ (P: 2 \sup A) (H1: ∀a:A. a ∈ P → a ∈ U)
+ (H2: ∀a:A. a ∈ P → ∀j: i ? a. C ? a j ≬ P):
+ ∀a:A. ∀p: a ∈ P. a ⋉ U ≝