+interpretation "covers set" 'covers a U = (cover_set cover ? a U).
+
+(*DOCBEGIN
+
+We will proceed similarly for the fish relation, but before going
+on it is better to give a short introduction to the proof mode of Matita.
+We define again the `cover_set` term, but this time we will build
+its body interactively. In λ-calculus Matita is based on, CIC, proofs
+and terms share the same syntax, and it thus possible to use the
+commands devoted to build proof term to build regular definitions.
+
+DOCEND*)
+
+
+ndefinition xcover_set :
+ ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0].
+(** screenshot "xcover-set-1". *)
+(*DOCBEGIN
+The system asks for a proof of the full statement, in an empty context.
+![xcover_set proof step ][xcover-set-1]
+The `#` command in the ∀-introduction rule, it gives a name to an
+assumption putting it in the context, and generates a λ-abstraction
+in the proof term.
+DOCEND*)
+#cover; #A; #C; #U; (** screenshot "xcover-set-2". *)
+(*DOCBEGIN
+![xcover_set proof step ][xcover-set-2]
+We have now to provide a proposition, and we exhibit it. We left
+a part of it implicit; since the system cannot infer it it will
+ask it later. Note that the type of `∀y:A.y ∈ C → ?` is a proposition
+whenever `?` is.
+DOCEND*)
+napply (∀y:A.y ∈ C → ?); (** screenshot "xcover-set-3". *)
+(*DOCBEGIN
+![xcover_set proof step ][xcover-set-3]
+The proposition we want to provide is an application of the
+cover relation we have abstracted in the context. The command
+`napply`, if the given term has not the expected type (in that
+case it is a product versus a proposition) it applies it to as many
+implicit arguments as necessary (in that case `? ? ?`).
+DOCEND*)
+napply cover; (** screenshot "xcover-set-4". *)
+(*DOCBEGIN
+![xcover_set proof step ][xcover-set-4]
+The system will now ask in turn the three implicit arguments
+passed to cover. The syntax `##[` allows to start a branching
+to tackle every sub proof individually, otherwise every command
+is applied to every subrpoof. The command `##|` switches to the next
+subproof and `##]` ends the branching.
+DOCEND*)
+##[ napply A;
+##| napply U;
+##| napply y;
+##]
+nqed.
+
+(*DOCBEGIN
+The definition of fish works exactly the same way as for cover, except
+that it is defined as a coinductive proposition.
+DOCEND*)