---

Step * 1 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. False@i
⊢ ⊥ ∈ A
BY
{ (RW assert_pushdownC (-1) THEN Auto) }

---

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.  False@i
\mvdash{}  \00DB  \mmember{}  A


By

---

Latex:
(RW  assert\_pushdownC  (-1)  THEN  Auto)

---

Home Index