---

Step * of Lemma comb_for_pi1_wf

λA,B,p,z. (fst(p)) ∈ A:Type ⟶ B:(A ⟶ Type) ⟶ p:(a:A × B[a]) ⟶ (↓True) ⟶ A
BY
{ (ProveOpCombinatorTyping Auto) `pi1_wf` }

---

Latex:

---

Latex:
\mlambda{}A,B,p,z.  (fst(p))  \mmember{}  A:Type  {}\mrightarrow{}  B:(A  {}\mrightarrow{}  Type)  {}\mrightarrow{}  p:(a:A  \mtimes{}  B[a])  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  A


By

---

Latex:
(ProveOpCombinatorTyping  Auto)  `pi1\_wf`

---

Home Index