---

Step * of Lemma term_accum_varterm_lemma

No Annotations
∀p,M,v,varcase,Q:Top.
  (term-accum(varterm(v) with p)
   p,f,vs,xxx.Q[p;f;vs;xxx]
   varterm(x) with p ⇒ varcase[p;x]
   mkterm(f,bts) with p ⇒ xxx.M[p;f;bts;xxx] ~ varcase[p;v])
BY
{ (Intros THEN Computation) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}p,M,v,varcase,Q:Top.
    (term-accum(varterm(v)  with  p)
      p,f,vs,xxx.Q[p;f;vs;xxx]
      varterm(x)  with  p  {}\mRightarrow{}  varcase[p;x]
      mkterm(f,bts)  with  p  {}\mRightarrow{}  xxx.M[p;f;bts;xxx]  \msim{}  varcase[p;v])


By

---

Latex:
(Intros  THEN  Computation)

---

Home Index