Hola.
Quizás lo que los complica es que cuando uno piensa la definición de un tipo inductivo (por ejemplo mirror para árboles binarios) tiene que dar todas las reglas de construcción del tipo que quiere generar. Esto es al revés que cuando uno piensa la definición de una función recursiva (por ejemplo inverse); en este caso uno va consumiendo la estructura (ya está construida) para computar algo (por ejemplo el espejo de un árbol).
Para el ejemplo:
Inductive bintree (A : Set) : Set :=
| empty_bt : bintree A
| node : bintree A -> A -> bintree A -> bintree A.
Inductive mirror (A : Set) : bintree A -> bintree A -> Prop :=
| mirror_empty : mirror A (empty_bt A) (empty_bt A)
| mirror_node :
forall (a : A) (t11 t12 t21 t22 : bintree A),
mirror A t11 t22 ->
mirror A t12 t21 ->
mirror A (node A t11 a t12) (node A t21 a t22).
Fixpoint inverse (A : Set) (t : bintree A):
bintree A :=
match t with
| empty_bt _ => empty_bt A
| node _ t1 a t2 => node A (inverse A t2) a (inverse A t1)
end.
Saludos, Carlos