---

Step * of Lemma comb_for_mk_perm_wf_a

λT,f,b,z. mk_perm(f;b) ∈ T:Type ⟶ f:(T ⟶ T) ⟶ b:(T ⟶ T) ⟶ (↓InvFuns(T;T;f;b)) ⟶ Perm(T)
BY
{ (ProveOpCombinatorTyping Auto) `mk_perm_wf_a` }

---

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{}InvFuns(T;T;f;b))  {}\mrightarrow{}  Perm(T)


By

---

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

---

Home Index