---

Step * of Lemma immediate-is-subterm

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

---

Latex:

---

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


By

---

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

---

Home Index