---

Step * of Lemma context-subset_functionality

No Annotations
∀[Gamma:j⊢]. ∀[a,b:{Gamma ⊢ _:𝔽}].  (Gamma ⊢ (a ⇐⇒ b) ⇒ {Gamma, a ⊢ _} ≡ {Gamma, b ⊢ _})
BY
{ (Auto THEN D -1 THEN D 0 THEN BLemma `context-subset-subtype` THEN Try (Fold `face-term-implies` 0) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[a,b:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].    (Gamma  \mvdash{}  (a  \mLeftarrow{}{}\mRightarrow{}  b)  {}\mRightarrow{}  \{Gamma,  a  \mvdash{}  \_\}  \mequiv{}  \{Gamma,  b  \mvdash{}  \_\})


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  D  0
  THEN  BLemma  `context-subset-subtype`
  THEN  Try  (Fold  `face-term-implies`  0)
  THEN  Auto)

---

Home Index