---

Step * of Lemma varterm_wf

No Annotations
∀[opr:Type]. ∀[v:varname()].  varterm(v) ∈ term(opr) supposing ¬(v = nullvar() ∈ varname())
BY
{ (InstLemma `term-ext` []
   THEN ParallelLast'
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN SubsumeC ⌜coterm-fun(opr;term(opr))⌝⋅
   THEN Auto
   THEN RepUR ``coterm-fun varterm`` 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[v:varname()].    varterm(v)  \mmember{}  term(opr)  supposing  \mneg{}(v  =  nullvar())


By

---

Latex:
(InstLemma  `term-ext`  []
  THEN  ParallelLast'
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  SubsumeC  \mkleeneopen{}coterm-fun(opr;term(opr))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  RepUR  ``coterm-fun  varterm``  0
  THEN  Auto)

---

Home Index