---

Step * 1 2 1 2 of Lemma band-wf-partial


1. a : partial(Base)
2. b : partial(𝔹)
3. a ∈ Top + Top
4. y : Top
5. a = (inr y ) ∈ (Top + Top)
6. is-exception(ff)
⊢ ↓False
BY
{ TACTIC:ImpossibleException  (-1) }

---

Latex:

---

Latex:

1.  a  :  partial(Base)
2.  b  :  partial(\mBbbB{})
3.  a  \mmember{}  Top  +  Top
4.  y  :  Top
5.  a  =  (inr  y  )
6.  is-exception(ff)
\mvdash{}  \mdownarrow{}False


By

---

Latex:
TACTIC:ImpossibleException    (-1)

---

Home Index