proposition: Theorem injection_left_son : 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: Proof. intros * H; change (left_son (hnode nat n 0 t1 t2) = left_son (hnode nat n 0 t3 t4)). now rewrite H. Qed.