---

Step * 1 of Lemma member-per-value


1. x : Base
2. (x)↓
⊢ x = x ∈ pertype(λx,b. ((x = b ∈ Base) ∧ (x)↓))
BY
{ (Refine_pertypeMemberEquality ⌜Type⌝⋅ THEN Try (Fold `per-set` 0) THEN Reduce 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  x  :  Base
2.  (x)\mdownarrow{}
\mvdash{}  x  =  x


By

---

Latex:
(Refine\_pertypeMemberEquality  \mkleeneopen{}Type\mkleeneclose{}\mcdot{}  THEN  Try  (Fold  `per-set`  0)  THEN  Reduce  0  THEN  Auto)\mcdot{}

---

Home Index