(13steps total) PrintForm Definitions Lemmas ElisTarskiPf A Sections NuprlLIB Doc

At: Tarski 1
1. Tr:(TermProp), tr:Term, L:(TermProp). RepsTruth(L; Tr; tr)
False
By:
Unfold `RepsTruth` 1
THEN
ExRepD
Generated subgoal:

11. Tr: TermProp
2. tr: Term
3. L: TermProp
4. S:Term. (t:Term. S = t) L(SUBX(tr; S))
5. RespectsNot(Tr; L)
6. ReflectsProp(Tr; tr; Tr)
False		11 steps

About:
functionpropfalseexists

(13steps total) PrintForm Definitions Lemmas ElisTarskiPf A Sections NuprlLIB Doc