suppose (n=m) (H).
suppose (S m = S p) (K).
suppose (n = S p) (L).
-obtain (S n) = (S m) by (eq_f ? ? ? ? ? H).
+conclude (S n) = (S m) by (eq_f ? ? ? ? ? H).
= (S p) by K.
= n by (sym_eq ? ? ? L)
done.
suppose (n=m) (H).
suppose (S m = S p) (K).
suppose (n = S p) (L).
-obtain (S n) = (S m) by _.
+conclude (S n) = (S m) by _.
= (S p) by _.
= n by _
done.
suppose (Node t1 t2 = Empty) (absurd).
(* Discriminate should really generate a theorem to be useful with
declarative tactics *)
- discriminate absurd.
+ destruct absurd.
by final
done.
qed.
\ No newline at end of file