---

Step * of Lemma unglue-term_wf2

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[T:{Gamma, phi ⊢ _}]. ∀[w:{Gamma, phi ⊢ _:(T ⟶ A)}].
∀[b:{Gamma ⊢ _:Glue [phi ⊢→ (T;w)] A}].
  (unglue(b) ∈ {Gamma ⊢ _:A[phi |⟶ app(w; b)]})
BY
{ (Intros
   THEN (Assert ⌜app(w; b) = unglue(b) ∈ {Gamma, phi ⊢ _:A}⌝⋅
   THENM (MemTypeCD THEN Try (Trivial) THEN MemCD' THEN Auto)
   )
   THEN Symmetry) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. T : {Gamma, phi ⊢ _}
5. w : {Gamma, phi ⊢ _:(T ⟶ A)}
6. b : {Gamma ⊢ _:Glue [phi ⊢→ (T;w)] A}
⊢ unglue(b) = app(w; b) ∈ {Gamma, phi ⊢ _:A}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[T:\{Gamma,  phi  \mvdash{}  \_\}].
\mforall{}[w:\{Gamma,  phi  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}].  \mforall{}[b:\{Gamma  \mvdash{}  \_:Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A\}].
    (unglue(b)  \mmember{}  \{Gamma  \mvdash{}  \_:A[phi  |{}\mrightarrow{}  app(w;  b)]\})


By

---

Latex:
(Intros
  THEN  (Assert  \mkleeneopen{}app(w;  b)  =  unglue(b)\mkleeneclose{}\mcdot{}  THENM  (MemTypeCD  THEN  Try  (Trivial)  THEN  MemCD'  THEN  Auto))
  THEN  Symmetry)

---

Home Index