Step
*
3
2
of Lemma
assert_of_band
.....wf..... 
1. p : 𝔹
2. ¬↑p
⊢ ⋂:False. 𝔹 ∈ Type
BY
{ Auto }
Latex:
Latex:
.....wf..... 
1.  p  :  \mBbbB{}
2.  \mneg{}\muparrow{}p
\mvdash{}  \mcap{}:False.  \mBbbB{}  \mmember{}  Type
By
Latex:
Auto
Home
Index