TypeOK => TypeOK' with no other assumptions

[tal...@xxxxxxxxx]

Hi. I'm new to TLA+ and just tried my first proof. It appeared to work, and everything went green, but it seemed a bit too easy. After simplifying things, I ended up with this, which also goes all green:

------------------------------- MODULE False -------------------------------

EXTENDS TLAPS

VARIABLE x

TypeOK == x = {}

THEOREM T0 ==
  ASSUME TypeOK
  PROVE  TypeOK'
  BY PTL DEF TypeOK

=============================================================================

Oddly, if I replace TypeOK with its definition then it no longer accepts it. It does still accept it if I remove the "DEF TypeOK" bit completely though.

Maybe I shouldn't be using "BY PTL" here, but could someone explain what this means?

This is Version 1.5.6 of 29 January 2018 and includes:
  - SANY Version 2.1 of 23 July 2017
  - TLC Version 2.12 of 29 January 2018
  - PlusCal Version 1.8 of 07 December 2015
  - TLATeX Version 1.0 of 20 September 2017

Thanks!