---

Step * of Lemma glue-term-1

No Annotations
∀[Gamma:j⊢]. ∀[T:{Gamma ⊢ _}]. ∀[t:{Gamma ⊢ _:T}]. ∀[A,a:Top].  (Gamma ⊢ glue [1(𝔽) ⊢→ t] a = t ∈ {Gamma ⊢ _:T})
BY
{ (InstLemma `glue-term-constraint` []
   THEN ParallelLast'
   THEN (D -1 With ⌜1(𝔽)⌝  THENA Auto)
   THEN RepeatFor 4 (ParallelLast')
   THEN SubsumeC ⌜{Gamma, 1(𝔽) ⊢ _:T}⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[T:\{Gamma  \mvdash{}  \_\}].  \mforall{}[t:\{Gamma  \mvdash{}  \_:T\}].  \mforall{}[A,a:Top].    (Gamma  \mvdash{}  glue  [1(\mBbbF{})  \mvdash{}\mrightarrow{}  t]  a  =  t)


By

---

Latex:
(InstLemma  `glue-term-constraint`  []
  THEN  ParallelLast'
  THEN  (D  -1  With  \mkleeneopen{}1(\mBbbF{})\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  4  (ParallelLast')
  THEN  SubsumeC  \mkleeneopen{}\{Gamma,  1(\mBbbF{})  \mvdash{}  \_:T\}\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index