-theorem injection_test3:
- ∀t,t'. tnode nat t tempty = tnode nat t' tempty → t = t'.
- intros;
- injection H;
- assumption.
-qed.
-
-theorem injection_test3:
- ∀t,t'.
- tnode nat (tnode nat t t') tempty = tnode nat (tnode nat t' tempty) tempty →
- t = t'.
- intros;
- injection H;
-
-