Step
*
1
1
1
1
of Lemma
page55-again
.....wf..... 
1. U : Type@i'
2. P : U ⟶ ℙ@i'
3. Q : U ⟶ ℙ@i'
4. x : U@i
⊢ x ∈ U
BY
{ Auto }
Latex:
Latex:
.....wf..... 
1.  U  :  Type@i'
2.  P  :  U  {}\mrightarrow{}  \mBbbP{}@i'
3.  Q  :  U  {}\mrightarrow{}  \mBbbP{}@i'
4.  x  :  U@i
\mvdash{}  x  \mmember{}  U
By
Latex:
Auto
Home
Index