-The reflexivity proof is trivial, it is enough to provide the ordinal 0
-as a witness, then ◃(U) reduces to U by definition, hence the conclusion.
+The reflexivity proof is trivial, it is enough to provide the ordinal `0`
+as a witness, then `◃(U)` reduces to `U` by definition,
+hence the conclusion. Note that `0` is between `(` and `)` to
+make it clear that it is a term (an ordinal) and not the number
+of the constructor we want to apply (that is the first and only one
+of the existential inductive type).