---

Step * 1 of Lemma top-subtype-function

.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. ¬A
4. x : Top@i
⊢ x ∈ A ⟶ B
BY
{ TACTIC:(Unfold `member` 0 THEN (Refine_functionExtensionality ⌜A⌝ `z'⋅ THEN Auto)⋅) }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  A  :  Type
2.  B  :  Type
3.  \mneg{}A
4.  x  :  Top@i
\mvdash{}  x  \mmember{}  A  {}\mrightarrow{}  B


By

---

Latex:
TACTIC:(Unfold  `member`  0  THEN  (Refine\_functionExtensionality  \mkleeneopen{}A\mkleeneclose{}  `z'\mcdot{}  THEN  Auto)\mcdot{})

---

Home Index