---

Step * of Lemma csm-pres-v

No Annotations
∀[G:j⊢]. ∀[phi:{G ⊢ _:𝔽}]. ∀[T:{G.𝕀 ⊢ _}]. ∀[t:{G.𝕀, (phi)p ⊢ _:T}]. ∀[t0:{G ⊢ _:(T)[0(𝕀)][phi |⟶ t[0]]}].
∀[cT:G.𝕀 ⊢ Compositon(T)]. ∀[H:j⊢]. ∀[s:H j⟶ G].
  ((pres-v(G;phi;t;t0;cT))s+ = pres-v(H;(phi)s;(t)s+;(t0)s;(cT)s+) ∈ {H.𝕀 ⊢ _:(T)s+[((phi)s)p |⟶ (t)s+]})
BY
{ (Intros THEN Unfold `pres-v` 0 THEN InstLemma `csm-fill_term` [⌜G⌝;⌜phi⌝;⌜T⌝;⌜cT⌝;⌜t⌝;⌜t0⌝;⌜H⌝;⌜s⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[phi:\{G  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[T:\{G.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[t:\{G.\mBbbI{},  (phi)p  \mvdash{}  \_:T\}].
\mforall{}[t0:\{G  \mvdash{}  \_:(T)[0(\mBbbI{})][phi  |{}\mrightarrow{}  t[0]]\}].  \mforall{}[cT:G.\mBbbI{}  \mvdash{}  Compositon(T)].  \mforall{}[H:j\mvdash{}].  \mforall{}[s:H  j{}\mrightarrow{}  G].
    ((pres-v(G;phi;t;t0;cT))s+  =  pres-v(H;(phi)s;(t)s+;(t0)s;(cT)s+))


By

---

Latex:
(Intros
  THEN  Unfold  `pres-v`  0
  THEN  InstLemma  `csm-fill\_term`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}cT\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}t0\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index