TATTICHE
+ - tattiche e fallimenti: una tattica che non progredisce dovrebbe fallire,
+ giusto?
- comportamento di tutte le tattiche nei confronti dei let-in
- tattica unfold su rel a let-in bound variables
- theorem t: True. elim x. ==> BOOM! unificazione di una testa flessibile con