+interpretation "char" 'subset p = (mk_powerset ? p).
+
+interpretation "pwset" 'powerset a = (powerset a).
+
+interpretation "in" 'mem a X = (char ? X a).
+
+definition subseteq ≝ λA.λu,v:\Omega \sup A.∀x.x ∈ u → x ∈ v.
+
+interpretation "subseteq" 'subseteq u v = (subseteq ? u v).
+
+definition overlaps ≝ λA.λU,V : Ω \sup A. exT2 ? (λx.x ∈ U) (λx.x ∈ V).
+
+interpretation "overlaps" 'overlaps u v = (overlaps ? u v).
+
+definition intersect ≝ λA.λu,v:Ω\sup A.{ y | y ∈ u ∧ y ∈ v }.
+
+interpretation "intersect" 'intersects u v = (intersect ? u v).
+
+record axiom_set : Type ≝ {
+ A:> Type;
+ i: A → Type;
+ C: ∀a:A. i a → Ω \sup A
+}.
+
+inductive for_all (A: axiom_set) (U,V: Ω \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: \Omega \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: \Omega \sup A.λP:\Omega \sup A.
+ λH1: U ⊆ 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 : \Omega \sup A) (fish: A → CProp) : CProp ≝
+ found : ∀a. a ∈ V → fish a → ex_such A U V fish.
+
+coinductive fish (A:axiom_set) (U: \Omega \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: \Omega \sup A)
+ (P: Ω \sup A) (H1: P ⊆ U)
+ (H2: ∀a:A. a ∈ P → ∀j: i ? a. C ? a j ≬ P):
+ ∀a:A. ∀p: a ∈ P. a ⋉ U ≝