Matemática Discreta 2: dura de pelar

En esto teño o coco medito últimamente. Dígoo para que non vos extrañedes se me vedes comportarme raro e tal.


(* A la función mem se le pasa un elemento de tipo Z (Set) y un árbol s. Se aplica recursivamente ({struct s}) sobre el árbol s, y éste tiene que ser estructuralmente más pequeño que el árbol de la llamada anterior. Devuelve un bool. La función mem devuelve true si el elemento de tipo Z se encuentra en el árbol a través de la hipótesis compare y de order, en caso contrario devuelve false *)

Fixpoint mem (x:Z) (s:arbol) {struct s} : bool :=
match s with
| Empty => false
| Node l y r => match compare x y with
| Lt => mem x l
| Eq => true
| Gt => mem x r
end
end.

Hint Resolve mem.