---

Step * of Lemma trivial-subterm

No Annotations
∀[opr:Type]. ∀f:opr. ∀bts:bound-term(opr) List. ∀i:ℕ||bts||.  snd(bts[i]) << mkterm(f;bts)
BY
{ (Auto THEN BLemma `immediate-is-subterm` THEN Auto THEN D 0 With ⌜f⌝  THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}f:opr.  \mforall{}bts:bound-term(opr)  List.  \mforall{}i:\mBbbN{}||bts||.    snd(bts[i])  <<  mkterm(f;bts)


By

---

Latex:
(Auto  THEN  BLemma  `immediate-is-subterm`  THEN  Auto  THEN  D  0  With  \mkleeneopen{}f\mkleeneclose{}    THEN  Auto)

---

Home Index