Hola, estoy trancado con este ejercicio.
Section Ejercicio18.
Variable A : Set.
Inductive Tree_ : Set :=
| nullT : Tree_
| consT : A -> Tree_ -> Tree_ -> Tree_.
La idea es definir un predicado inductivo:
Inductive isSubTree : Tree_ -> Tree_ -> Prop := ...
Yo definí dicho predicado, pienso que es correcto, pero no logro probar la parte 3 que pide la transitividad. ¿Alguna pista?
Saludos,
Jairo.