---

Step * of Lemma per-type-family_wf

∀[A:Type]. ∀[B:Type supposing A].  (per-type-family(B) ∈ per-function(A;a.Type))
BY
{ ((Intros THEN Unhide) THEN Unfold `per-type-family` 0) }

1
1. A : Type
2. B : Type supposing A
⊢ λx.B ∈ per-function(A;a.Type)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:Type  supposing  A].    (per-type-family(B)  \mmember{}  per-function(A;a.Type))


By

---

Latex:
((Intros  THEN  Unhide)  THEN  Unfold  `per-type-family`  0)

---

Home Index