---

Step * of Lemma term_accum1_varterm_lemma

No Annotations
∀p,v,M,vcase,Q:Top.
  (term-accum1(varterm(v))a,b,c,d.Q[a;b;c;d]varterm(v) with p ⇒ vcase[v;p]mkterm(f,bts) with p ⇒ L.M[p;f;bts;L] p 
  ~ vcase[v;p])
BY
{ (Intros THEN Computation) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}p,v,M,vcase,Q:Top.
    (term-accum1(varterm(v))
      a,b,c,d.Q[a;b;c;d]
      varterm(v)  with  p  {}\mRightarrow{}  vcase[v;p]
      mkterm(f,bts)  with  p  {}\mRightarrow{}  L.M[p;f;bts;L] 
      p  \msim{}  vcase[v;p])


By

---

Latex:
(Intros  THEN  Computation)

---

Home Index