---

Step * of Lemma TC-trans

∀[Dom:Type]. ∀[R:Dom ─→ Dom ─→ ℙ]. ∀[x,y,z:Dom].  (TC(λa,b.R a b)(x,y) ⇒ TC(λa,b.R a b)(y,z) ⇒ TC(λa,b.R a b)(x,z))
BY
{ (Auto
   THEN All (Unfold `TC`)
   THEN (InstLemma `transitive-closure-transitive` [⌈Dom⌉;⌈λ2x y.R x y⌉]⋅ THENA Auto)
   THEN Unfold `so_lambda` (-1)
   THEN All (Fold `infix_ap`)
   THEN Auto) }

---

Latex:


\mforall{}[Dom:Type].  \mforall{}[R:Dom  {}\mrightarrow{}  Dom  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[x,y,z:Dom].
    (TC(\mlambda{}a,b.R  a  b)(x,y)  {}\mRightarrow{}  TC(\mlambda{}a,b.R  a  b)(y,z)  {}\mRightarrow{}  TC(\mlambda{}a,b.R  a  b)(x,z))


By

(Auto
  THEN  All  (Unfold  `TC`)
  THEN  (InstLemma  `transitive-closure-transitive`  [\mkleeneopen{}Dom\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.R  x  y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `so\_lambda`  (-1)
  THEN  All  (Fold  `infix\_ap`)
  THEN  Auto)

---

Home Index