---

Step * of Lemma csm-face-term-implies

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}].
  ∀[H:j⊢]. ∀[s:H j⟶ Gamma].  H ⊢ ((phi)s ⇒ (psi)s) supposing Gamma ⊢ (phi ⇒ psi)
BY
{ (Auto THEN D 0 THEN Auto THEN (RWO  "csm-ap-term-at" (-1) THENA Auto) THEN RWO  "csm-ap-term-at" 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi,psi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].
    \mforall{}[H:j\mvdash{}].  \mforall{}[s:H  j{}\mrightarrow{}  Gamma].    H  \mvdash{}  ((phi)s  {}\mRightarrow{}  (psi)s)  supposing  Gamma  \mvdash{}  (phi  {}\mRightarrow{}  psi)


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (RWO    "csm-ap-term-at"  (-1)  THENA  Auto)
  THEN  RWO    "csm-ap-term-at"  0
  THEN  Auto)

---

Home Index