suppose (Node t1 t2 = Empty) (absurd).
(* Discriminate should really generate a theorem to be useful with
declarative tactics *)
suppose (Node t1 t2 = Empty) (absurd).
(* Discriminate should really generate a theorem to be useful with
declarative tactics *)