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