---

Step * 1 of Lemma base-member-partial


1. [A] : Type
2. [%] : value-type(A)
3. [a] : Base
4. [%1] : a ∈ A supposing (a)↓
⊢ a ∈ partial(A) supposing ¬is-exception(a)
BY
{ TACTIC:D 0 }

1
1. A : Type
2. value-type(A)
3. a : Base
4. a ∈ A supposing (a)↓
5. ¬is-exception(a)
⊢ a ∈ partial(A)

2
.....wf..... 
1. A : Type
2. value-type(A)
3. a : Base
4. a ∈ A supposing (a)↓
⊢ istype(¬is-exception(a))

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [\%]  :  value-type(A)
3.  [a]  :  Base
4.  [\%1]  :  a  \mmember{}  A  supposing  (a)\mdownarrow{}
\mvdash{}  a  \mmember{}  partial(A)  supposing  \mneg{}is-exception(a)


By

---

Latex:
TACTIC:D  0

---

Home Index