---

Step * 1 of Lemma subtype_rel-per-set


1. A : Type
2. B : A ⟶ Type
3. x : per-set(A;a.B[a])@i
4. per-set(A;a.B[a]) ∈ Type
⊢ x ∈ A
BY
{ (PointwiseFunctionality 3 THEN Try (Unhide) THEN PerHD (-2) THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  x  :  per-set(A;a.B[a])@i
4.  per-set(A;a.B[a])  \mmember{}  Type
\mvdash{}  x  \mmember{}  A


By

---

Latex:
(PointwiseFunctionality  3  THEN  Try  (Unhide)  THEN  PerHD  (-2)  THEN  Auto)

---

Home Index