+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 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. coversl A U (C ? a j) → covers A U a
+with coversl : (2 \sup A) → CProp ≝
+ iter: ∀V:2 \sup A.(∀a:A.a ∈ V → covers A U a) → coversl A U V.
+
+notation "hvbox(a break ◃ b)" non associative with precedence 45
+for @{ 'covers $a $b }.
+
+interpretation "covers" 'covers a U = (covers _ U a).
+interpretation "coversl" 'covers A U = (coversl _ U A).
+
+definition covers_elim ≝
+ λA:axiom_set.λU: 2 \sup A.λP:A → CProp.
+ λH1:∀a:A. a ∈ U → P a.
+ λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → (∀b. b ∈ C ? a j → P b) → P a.
+ let rec aux (a:A) (p:a ◃ U) on p : P a ≝
+ match p return λaa.λ_:aa ◃ U.P aa with
+ [ refl a q ⇒ H1 a q
+ | infinity a j q ⇒ H2 a j q (auxl (C ? a j) q)
+ ]
+ and auxl (V: 2 \sup A) (q: V ◃ U) on q : ∀b. b ∈ V → P b ≝
+ match q return λVV.λ_:VV ◃ U.∀b. b ∈ VV → P b with
+ [ iter VV f ⇒ λb.λr. aux b (f b r) ]
+ in
+ aux.
+
+coinductive fish (A:axiom_set) (U: 2 \sup A) : A → Prop ≝
+ mk_fish: ∀a:A. (a ∈ U ∧ ∀j: i ? a. ∃y: A. y ∈ C ? a j ∧ fish A U y) → fish A U a.
+
+notation "hvbox(a break ⋉ b)" non associative with precedence 45
+for @{ 'fish $a $b }.
+
+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. ∃y: A. y ∈ C ? a j ∧ y ∈ P) :
+ ∀a:A. ∀p: a ∈ P. a ⋉ U ≝