---

Step * of Lemma base-member-partial

∀[A:Type]. ∀[a:Base]. (a ∈ partial(A)) supposing ((¬is-exception(a)) and a ∈ A supposing (a)↓) supposing value-type(A)
BY
{ TACTIC:RepeatFor 4 ((UD THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}[a:Base].  (a  \mmember{}  partial(A))  supposing  ((\mneg{}is-exception(a))  and  a  \mmember{}  A  supposing  (a)\mdownarrow{})  supposing  valu\000Ce-type(A)


By

---

Latex:
TACTIC:RepeatFor  4  ((UD  THENA  Auto))

---

Home Index