---

Step * of Lemma comb_for_mk_perm_wf

λT,f,b,z. mk_perm(f;b) ∈ T:Type ⟶ f:(T ⟶ T) ⟶ b:(T ⟶ T) ⟶ (↓True) ⟶ perm_sig(T)
BY
{ (ProveOpCombinatorTyping Auto) `mk_perm_wf` }

---

Latex:

---

Latex:
\mlambda{}T,f,b,z.  mk\_perm(f;b)  \mmember{}  T:Type  {}\mrightarrow{}  f:(T  {}\mrightarrow{}  T)  {}\mrightarrow{}  b:(T  {}\mrightarrow{}  T)  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  perm\_sig(T)


By

---

Latex:
(ProveOpCombinatorTyping  Auto)  `mk\_perm\_wf`

---

Home Index