Das Lemma delete deletes muss nicht vollständig bewiesen sein, um das Testat zu bekommen. Es muss jedoch ein sinnvoller Beweisansatz vorliegen. Dies bedeutet konkret: Wenn man den Beweis mit "Verify" startet, enthält der Goalterm (mindestens) vier Teilaussagen ("maximal eingerückte boolesche Teilterme"). Mindestens eine dieser Teilaussagen muss bewiesen werden. Grob gesagt betreffen die Teilaussagen folgende Fälle:
- Es wird nichts im linken Teilbaum gefunden.
- Es wird nichts im rechten Teilbaum gefunden.
- Beim Suchen in "add.left(t, dest)" wird man in "t" fündig.
- Beim Suchen in "add.left(t, dest)" wird man in "dest" fündig.