---

Step * 1 1 of Lemma glue-type-term-subtype

.....subterm..... T:t
1:n
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. T : {Gamma, phi ⊢ _}
5. w : {Gamma, phi ⊢ _:(T ⟶ A)}
6. Gamma, phi ⊢ Glue [phi ⊢→ (T;w)] A = T
7. x : {Gamma ⊢ _:Glue [phi ⊢→ (T;w)] A}
⊢ x ∈ {Gamma, phi ⊢ _:T}
BY
{ (RepeatFor 2 (MoveToConcl (-1)) THEN (GenConclTerm ⌜Glue [phi ⊢→ (T;w)] A⌝⋅ THENA Auto) THEN All Thin THEN Intros) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. T : {Gamma, phi ⊢ _}
4. v : {Gamma ⊢ _}
5. Gamma, phi ⊢ v = T
6. x : {Gamma ⊢ _:v}
⊢ x ∈ {Gamma, phi ⊢ _:T}

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
4.  T  :  \{Gamma,  phi  \mvdash{}  \_\}
5.  w  :  \{Gamma,  phi  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}
6.  Gamma,  phi  \mvdash{}  Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A  =  T
7.  x  :  \{Gamma  \mvdash{}  \_:Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A\}
\mvdash{}  x  \mmember{}  \{Gamma,  phi  \mvdash{}  \_:T\}


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))
  THEN  (GenConclTerm  \mkleeneopen{}Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Intros)

---

Home Index