# Manual injection on variably dependent types

Using the type `htree> given by the following definition:`

`
`Inductive htree (A:Set) : nat -> Set :=
hleaf : A -> (htree A O)
| hnode : forall n:nat, A -> htree A n -> htree A n -> htree A (S n).

Prove the following statement:

Theorem injection_first_htree:
forall (n : nat) (t1 t2 t3 t4 : htree nat n),
hnode nat n O t1 t2 = hnode nat n O t3 t4 -> t1 = t3.

## Solution

This file

## Note

Use tactics to define the injection function that maps a tree down
to one of its subterms: the `Case` tactic provides the
relevant dependent pattern matching construct.

Yves Bertot
Last modified: Sat Aug 2 11:17:27 MEST 2003