- suppose (O < size (Node t1 t2)) (Hyp).
- (*BUG: that is equivalent to missed here *)
- unfold Not.
- suppose (Node t1 t2 = Empty) (absurd).
- (* Discriminate should really generate a theorem to be useful with
- declarative tactics *)
- discriminate absurd.
+ suppose (O < size (Node t1 t2)) (useless).
+ we need to prove (Node t1 t2 ≠ Empty) (final)
+ or equivalently (Node t1 t2 = Empty → False).
+ suppose (Node t1 t2 = Empty) (absurd).
+ (* Discriminate should really generate a theorem to be useful with
+ declarative tactics *)
+ discriminate absurd.
+ by final
+ done.