The Coq mailing list

[Pierre Lescanne <Pierre.Lescanne AT laposte.net>]

May I propose my solution that does not use this rather complex 
"first_of_htree" function:

Lemma injection : forall (n:nat) (t1 t2 t3 t4: htree nat n),
 hnode nat n 0 t1 t2 = hnode nat n 0 t3 t4 -> t1=t3.
Proof.
intros n t1 t2 t3 t4 H.
change (let fst_proj:= fun (m:nat) (t: htree nat m) =>
 match t in htree _ x return htree nat (pred x) with | hleaf v => hleaf 
nat v | hnode k _ t' _ => t' end
 in fst_proj (S n) (hnode nat n 0 t1 t2) = fst_proj (S n) (hnode nat n 
0 t3 t4)).
rewrite H.
trivial.
Qed.

OK I agree that the trick is to find the right function in the change 
tactic.

Pierre