---

Step * of Lemma comb_for_reduce2_wf

λA,T,L,k,i,f,z. reduce2(f;k;i;L) ∈ A:Type ⟶ T:Type ⟶ L:(T List) ⟶ k:A ⟶ i:ℕ ⟶ f:(T ⟶ {i..i + ||L||-} ⟶ A ⟶ A) ⟶\000C (↓True) ⟶ A
BY
{ (ProveOpCombinatorTyping Auto) `reduce2_wf` }

---

Latex:

---

Latex:
\mlambda{}A,T,L,k,i,f,z.  reduce2(f;k;i;L)  \mmember{}  A:Type
{}\mrightarrow{}  T:Type
{}\mrightarrow{}  L:(T  List)
{}\mrightarrow{}  k:A
{}\mrightarrow{}  i:\mBbbN{}
{}\mrightarrow{}  f:(T  {}\mrightarrow{}  \{i..i  +  ||L||\msupminus{}\}  {}\mrightarrow{}  A  {}\mrightarrow{}  A)
{}\mrightarrow{}  (\mdownarrow{}True)
{}\mrightarrow{}  A


By

---

Latex:
(ProveOpCombinatorTyping  Auto)  `reduce2\_wf`

---

Home Index