[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