```
Inductive tree' (X : Type) : Type :=
| leaf' (x : X)
| node' (t : tree (X * X)).
Check tree'_ind.
(* tree'_ind *)
(* : forall (X : Type) (P : tree' X -> Prop), *)
(* (forall x : X, P (leaf' X x)) -> (forall t : tree (X * X), P (node' X t)) -> forall t : tree' X, P t *)
```

What is the useful induction principle for such parameterized but not homogeneous inductive types?

yiyuan-cao has marked this topic as unresolved.

Should `tree`

be `tree'`

? Your given example is homogeneous

Last updated: Jun 13 2024 at 19:02 UTC