---

Step * of Lemma outr-class_wf

∀[Info,A:Type]. ∀[X:EClass(Top + A)].  (outr-class(X) ∈ EClass(A))
BY
{ ProveWfLemma }

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. ↑((λx.(¬bisl(x))) (inl x1))@i
⊢ ⊥ ∈ A

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[X:EClass(Top  +  A)].    (outr-class(X)  \mmember{}  EClass(A))


By

---

Latex:
ProveWfLemma

---

Home Index