---

Step * of Lemma comb_for_wellfounded_wf

λA,r,z. WellFnd{i}(A;x,y.r[x;y]) ∈ A:Type ⟶ r:(A ⟶ A ⟶ ℙ) ⟶ (↓True) ⟶ ℙ'
BY
{ (ProveOpCombinatorTyping Auto{1,3}-1) `wellfounded_wf` }

---

Latex:

---

Latex:
\mlambda{}A,r,z.  WellFnd\{i\}(A;x,y.r[x;y])  \mmember{}  A:Type  {}\mrightarrow{}  r:(A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbP{}'


By

---

Latex:
(ProveOpCombinatorTyping  Auto\{1,3\}-1)  `wellfounded\_wf`

---

Home Index