[vinz@hauru v8.3]$ bin/coqtop
Welcome to Coq v8.3 (14088)

Coq < Require Import List.

Coq < Scheme Equality for list.
list_beq is defined
list_eq_dec is defined

Coq < Check list_eq_dec.
list_eq_dec
     : forall (A : Type) (eq_A : A -> A -> bool),
       (forall x y : A, eq_A x y = true -> x = y) ->
       (forall x y : A, x = y -> eq_A x y = true) ->
       forall x y : list A, {x = y} + {x <> y}

Coq < Inductive tree (A : Type) : Type :=
Coq < | node : A -> tree A
Coq < | leafs : list A -> tree A.
tree is defined
tree_rect is defined
tree_ind is defined
tree_rec is defined

Coq < Scheme Equality for tree.
tree_beq is defined
tree_eq_dec is defined