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.
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.