-![fish proof step][def-fish-rec-5-1]
-![fish proof step][def-fish-rec-6]
-![fish proof step][def-fish-rec-7]
-![fish proof step][def-fish-rec-8]
-![fish proof step][def-fish-rec-9]
-DOCEND*)
+
+D[def-fish-rec-5-1]
+The goal is now the existence of an a point in `𝐂 a i` fished by `U`.
+We thus need to use the introduction rulle for the existential quantifier.
+In CIC it is a defined notion, that is an inductive type with just
+one constructor (one introduction rule) holding the witness and the proof
+that the witness satisfies a proposition.
+
+> ncheck Ex.
+
+Instead of trying to remember the name of the constructor, that should
+be used as the argument of `napply`, we can ask the system to find by
+itself the constructor name and apply it with the `@` tactic.
+Note that some inductive predicates, like the disjunction, have multiple
+introduction rules, and thus `@` can be followed by a number identifying
+the constructor.
+
+D[def-fish-rec-6]
+After choosing `x` as the witness, we have to prove a conjunction,
+and we again apply the introduction rule for the inductively defined
+predicate `∧`.
+
+D[def-fish-rec-7]
+The left hand side of the conjunction is trivial to prove, since it
+is already in the context. The right hand side needs to perform
+the co-recursive call.
+
+D[def-fish-rec-9]
+The co-recursive call needs some arguments, but all of them live
+in the context. Instead of explicitly mention them, we use the
+`nassumption` tactic, that simply tries to apply every context item.
+
+D*)