---

Step * 1 1 1 of Lemma TC-ind


1. [Dom] : Type
2. [B] : Dom ─→ ℙ
3. [R] : Dom ─→ Dom ─→ ℙ
4. ∀x,y:Dom.  ((R x y) ⇒ (B x) ⇒ (B y))@i
5. x : Dom@i
6. y : Dom@i
7. TC(λa,b. (R a b)) x y@i
8. B x@i
9. ∀x,y:Dom.  ((x TC(λ2x y.R x y) y) ⇒ (B x) ⇒ (B y))
⊢ B y
BY
{ ((Unfold `so_lambda` -1 THEN RepUR ``infix_ap`` -1) THEN InstHyp [⌈x⌉;⌈y⌉] (-1)⋅ THEN Auto) }

---

Latex:



1.  [Dom]  :  Type
2.  [B]  :  Dom  {}\mrightarrow{}  \mBbbP{}
3.  [R]  :  Dom  {}\mrightarrow{}  Dom  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x,y:Dom.    ((R  x  y)  {}\mRightarrow{}  (B  x)  {}\mRightarrow{}  (B  y))@i
5.  x  :  Dom@i
6.  y  :  Dom@i
7.  TC(\mlambda{}a,b.  (R  a  b))  x  y@i
8.  B  x@i
9.  \mforall{}x,y:Dom.    ((x  TC(\mlambda{}\msubtwo{}x  y.R  x  y)  y)  {}\mRightarrow{}  (B  x)  {}\mRightarrow{}  (B  y))
\mvdash{}  B  y


By

((Unfold  `so\_lambda`  -1  THEN  RepUR  ``infix\_ap``  -1)  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)

---

Home Index