---

Step * of Lemma comb_for_comp_perm_wf

λT,p,q,z. p O q ∈ T:Type ⟶ p:Perm(T) ⟶ q:Perm(T) ⟶ (↓True) ⟶ Perm(T)
BY
{ (ProveOpCombinatorTyping Auto) `comp_perm_wf` }

---

Latex:

---

Latex:
\mlambda{}T,p,q,z.  p  O  q  \mmember{}  T:Type  {}\mrightarrow{}  p:Perm(T)  {}\mrightarrow{}  q:Perm(T)  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  Perm(T)


By

---

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

---

Home Index