---

Step * 1 of Lemma outr-class_wf


1. Info : Type
2. A : Type
3. X : EClass(Top + A)
4. b : bag(Top + A)@i
5. ∀x:Top + A. (↑((λx.(¬bisl(x))) x) ∈ 𝕌{[1 | i 0]})
6. x1 : Top@i
7. ↑((λx.(¬bisl(x))) (inl x1))@i
⊢ ⊥ ∈ A
BY
{ Reduce (-1) }

1
1. Info : Type
2. A : Type
3. X : EClass(Top + A)
4. b : bag(Top + A)@i
5. ∀x:Top + A. (↑((λx.(¬bisl(x))) x) ∈ 𝕌{[1 | i 0]})
6. x1 : Top@i
7. False@i
⊢ ⊥ ∈ A

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  X  :  EClass(Top  +  A)
4.  b  :  bag(Top  +  A)@i
5.  \mforall{}x:Top  +  A.  (\muparrow{}((\mlambda{}x.(\mneg{}\msubb{}isl(x)))  x)  \mmember{}  \mBbbU{}\{[1  |  i  0]\})
6.  x1  :  Top@i
7.  \muparrow{}((\mlambda{}x.(\mneg{}\msubb{}isl(x)))  (inl  x1))@i
\mvdash{}  \00DB  \mmember{}  A


By

---

Latex:
Reduce  (-1)

---

Home Index