gen_tree: add comment explaining intended usage

#227 (closed) shows that this is not obvious, and this is entirely fair.

However, this seems surprisingly inconsistent. The more consistent thing would be to use a GenNode for each constructor, including non-recursive ones; then one also does not have to ever duplicate types in the big sum that is T and one can always use the number in the node to indicate the constructor. Should we recommend that instead? If so, we should probably adjust the users, at least in the core std++ and Iris repos, to follow that pattern. We might even want to use a different definition then:

Inductive gen_tree (T : Type) : Type :=
  | GenNode : nat → list T → list (gen_tree T) → gen_tree T.

The list of T can be used to store arbitrary data of other types, and then the list of children is used for recursion only.

stdpp/countable.v

@@ -313,6 +313,18 @@ Qed.
 (** ** Generic trees *)
 Local Close Scope positive.
 
+(** This type can help you construct a [Countable] instance for an arbitrary
+(even recursive) inductive datatype. The idea is tht you make [T] something like
+[T1 + T2 + ...], covering all the data types that can be contained inside your
+type.
+- Each non-recursive constructor to a [GenLeaf]. Different constructors must use
+  different variants of [T] to ensure they remain distinguishable!
+- Each recursive constructor to a [GenNode] where the [nat] is a (typically
+  small) constant representing the constructor itself, and then all the data in
+  the constructor (recursive or otherwise) is put into child nodes.
+
+This data type is the same as `GenTree.tree` in mathcomp, see
+https://github.com/math-comp/math-comp/blob/master/ssreflect/choice.v *)
 Inductive gen_tree (T : Type) : Type :=
   | GenLeaf : T → gen_tree T
   | GenNode : nat → list (gen_tree T) → gen_tree T.