---

Step * of Lemma subterm_transitivity

No Annotations
∀[opr:Type]. ∀s,t,r:term(opr).  (s << t ⇒ t << r ⇒ s << r)
BY
{ ((Unfold `subterm` 0
    THEN (Unfold `subterm-rel` 0 THEN Auto)
    THEN InstLemma `transitive-closure-transitive` [⌜term(opr)⌝;⌜λs,t. s < t⌝]⋅)
   THEN Auto
   ) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}s,t,r:term(opr).    (s  <<  t  {}\mRightarrow{}  t  <<  r  {}\mRightarrow{}  s  <<  r)


By

---

Latex:
((Unfold  `subterm`  0
    THEN  (Unfold  `subterm-rel`  0  THEN  Auto)
    THEN  InstLemma  `transitive-closure-transitive`  [\mkleeneopen{}term(opr)\mkleeneclose{};\mkleeneopen{}\mlambda{}s,t.  s  <  t\mkleeneclose{}]\mcdot{})
  THEN  Auto
  )

---

Home Index