Step
*
2
of Lemma
Russell_wf
.....subterm..... T:t
2:n
1. T : Type ⋂ Base
⊢ ¬(T ∈ T) ∈ 𝕌'
BY
{ (MemCD THEN RW (AddrC [2] UnfoldTopAbC) 0 THEN BLemma `equal-wf-base` THEN Auto) }
Latex:
Latex:
.....subterm..... T:t
2:n
1. T : Type \mcap{} Base
\mvdash{} \mneg{}(T \mmember{} T) \mmember{} \mBbbU{}'
By
Latex:
(MemCD THEN RW (AddrC [2] UnfoldTopAbC) 0 THEN BLemma `equal-wf-base` THEN Auto)
Home
Index