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. injection H; intros H1 H2. dependent rewrite <- H1. trivial. Qed.
imports: ZArith List Arith Lia Zwf Relations JMeq