(that state the existence of a ?1 such that ...) *)
theorem injection_test3:
∀t,t'. tnode nat t tempty = tnode nat t' tempty → t = t'.
(that state the existence of a ?1 such that ...) *)
theorem injection_test3:
∀t,t'. tnode nat t tempty = tnode nat t' tempty → t = t'.