---

Step * 1 of Lemma all_wf


1. ∀[A:Type]. ∀[B:A ⟶ Type].  (a:A ⟶ B[a] ∈ Type)
⊢ ∀[A:Type]. ∀[B:A ⟶ Type].  (a:A ⟶ B[a] ∈ Type)
BY
{ Trivial }

---

Latex:

---

Latex:

1.  \mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].    (a:A  {}\mrightarrow{}  B[a]  \mmember{}  Type)
\mvdash{}  \mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].    (a:A  {}\mrightarrow{}  B[a]  \mmember{}  Type)


By

---

Latex:
Trivial

---

Home Index