---

Step * of Lemma hereditarily_functionality_wrt_subterm

No Annotations
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ].  ∀t,s:term(opr).  (s << t ⇒ hereditarily(opr;s.P[s];t) ⇒ hereditarily(opr;s.P[s];s))
BY
{ (Auto THEN ParallelLast THEN Auto THEN BackThruSomeHyp THEN InstLemma `subterm_transitivity` [⌜opr⌝]⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  ParallelLast
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  InstLemma  `subterm\_transitivity`  [\mkleeneopen{}opr\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index