proposition: Theorem any_height_inj2' {A:Type} : forall (n1 n2:nat)(t1:htree A n1)(t2:htree A n2), any_height n1 t1 = any_height n2 t2 -> JMeq t1 t2.
proof: Proof. intros n1 n2 t1 t2 H. change (match any_height n2 t2 with | any_height n t => JMeq t1 t end); now rewrite <- H. Qed.
imports: ZArith List Arith Lia Zwf Relations JMeq