---

Step * of Lemma member-per-value

∀[x:Base]. x ∈ per-value() supposing (x)↓
BY
{ TACTIC:(Auto THEN Unfold `per-value` 0 THEN Unfold `member` 0 THEN Unfold `per-set` 0) }

1
1. x : Base
2. (x)↓
⊢ x = x ∈ pertype(λx,b. ((x = b ∈ Base) ∧ (x)↓))

---

Latex:

---

Latex:
\mforall{}[x:Base].  x  \mmember{}  per-value()  supposing  (x)\mdownarrow{}


By

---

Latex:
TACTIC:(Auto  THEN  Unfold  `per-value`  0  THEN  Unfold  `member`  0  THEN  Unfold  `per-set`  0)

---

Home Index