| | Who Cites ReflectsProp? |
|
| ReflectsProp | Def ReflectsProp(P; qP; Tr) ==  t,qt:Term. qt reps t   {Tr(qP/qt)  Tr(t)} |
| | | Thm* P:(Term  Prop), qP:Term, L:(TermProp). ReflectsProp(P; qP; L)  Prop |
|
| subx | Def t/e == t[e/X] |
| | | Thm* t,r:Term. t/r Term |
|
| iff | Def P Q == (P Q) & (P Q) |
| | | Thm* A,B:Prop. (A B) Prop |
|
| repst | Def x reps y == x reps y Term |
| | | Thm* t,x:Term. (t reps x) Prop |
|
| rev_implies | Def P Q == Q P |
| | | Thm* A,B:Prop. (A B) Prop |
|
| reps | Def x reps y t == x IN t & ref(x) = y t |
| | | Thm* t:(u Term), x:u. (t reps x u) Prop |
| | | Thm* t,x:Term. (t reps x Term) Prop |
