---

Step * of Lemma mkterm_wf

No Annotations
∀[Op:Type]. ∀[opr:Op]. ∀[bts:(varname() List × term(Op)) List].  (mkterm(opr;bts) ∈ term(Op))
BY
{ (InstLemma `term-ext` []
   THEN ParallelLast'
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN SubsumeC ⌜coterm-fun(Op;term(Op))⌝⋅
   THEN Auto
   THEN RepUR ``coterm-fun mkterm`` 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Op:Type].  \mforall{}[opr:Op].  \mforall{}[bts:(varname()  List  \mtimes{}  term(Op))  List].    (mkterm(opr;bts)  \mmember{}  term(Op))


By

---

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

---

Home Index