+ (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
+(** screenshot "def-fish-rec-1". *)
+(*DOCBEGIN
+![fish proof step][def-fish-rec-1]
+Note the first item of the context, it is the corecursive function we are
+defining. This item allows to perform the recursive call, but we will be
+allowed to do such call only after having generated a constructor of
+the fish coinductive type.
+
+We introduce `a` and `p`, and then return the fish constructor `cfish`.
+Since the constructor accepts two arguments, the system asks for them.
+DOCEND*)
+#a; #p; napply cfish; (** screenshot "def-fish-rec-2". *)
+(*DOCBEGIN
+![fish proof step][def-fish-rec-2]
+The first one is a proof that `a ∈ U`. This can be proved using `H1` and `p`.
+With the `nchange` tactic we change `H1` into an equivalent form (this step
+can be skipped, since the systeem would be able to unfold the definition
+of inclusion by itself)
+DOCEND*)
+##[ nchange in H1 with (∀b.b∈P → b∈U);
+
+ (** screenshot "def-fish-rec-2-1". *) napply H1;
+ (** screenshot "def-fish-rec-3". *) nassumption;
+(*DOCBEGIN
+![fish proof step][def-fish-rec-2-1]
+It is now clear that `H1` can be applied. Again `napply` adds two
+implicit arguments to `H1 ? ?`, obtaining a proof of `? ∈ U` given a proof
+that `? ∈ P`. Thanks to unification, the system understands that `?` is actually
+`a`, and it asks a proof that `a ∈ P`.
+![fish proof step][def-fish-rec-3]
+The `nassumption` tactic looks for the required proof in the context, and in
+that cases finds it in the last context position.
+
+We move now to the second branch of the proof, corresponding to the second
+argument of the `cfish` constructor.
+![fish proof step][def-fish-rec-4]
+DOCEND*)
+##| (** screenshot "def-fish-rec-4". *) #i; ncases (H2 a p i);
+ (** screenshot "def-fish-rec-5". *) #x; *; #xC; #xP;
+ (** screenshot "def-fish-rec-5-1". *) @;
+ ##[ (** screenshot "def-fish-rec-6". *) napply x
+ ##| (** screenshot "def-fish-rec-7". *)
+ @; ##[ napply xC;
+ ##| (** screenshot "def-fish-rec-8". *)
+ napply (fish_rec ? U P);
+ (** screenshot "def-fish-rec-9". *)
+ nassumption;
+ ##]
+ ##]