---

Step * of Lemma is-list-prop1

No Annotations
∀[t:Base]. t ∈ Base List supposing (is-list(t))↓
BY
{ TACTIC:(Intros THEN Try ((GenConcl ⌜is-list(t) = z ∈ Base⌝⋅ THEN Auto)) THEN Unhide) }

1
1. t : Base
2. (is-list(t))↓
⊢ t ∈ Base List

---

Latex:

---

Latex:
No  Annotations
\mforall{}[t:Base].  t  \mmember{}  Base  List  supposing  (is-list(t))\mdownarrow{}


By

---

Latex:
TACTIC:(Intros  THEN  Try  ((GenConcl  \mkleeneopen{}is-list(t)  =  z\mkleeneclose{}\mcdot{}  THEN  Auto))  THEN  Unhide)

---

Home Index