---

Step * of Lemma pres-c1_wf

No Annotations
∀[G:j⊢]. ∀[phi:{G ⊢ _:𝔽}]. ∀[A,T:{G.𝕀 ⊢ _}]. ∀[f:{G.𝕀 ⊢ _:(T ⟶ A)}]. ∀[t:{G.𝕀, (phi)p ⊢ _:T}].
∀[t0:{G ⊢ _:(T)[0(𝕀)][phi |⟶ t[0]]}]. ∀[cA:composition-function{j:l,i:l}(G.𝕀;A)].
  (pres-c1(G;phi;f;t;t0;cA) ∈ {G ⊢ _:(A)[1(𝕀)][phi |⟶ app(f; t)[1]]})
BY
{ (Intros
   THEN Unhide
   THEN Unfold `pres-c1` 0
   THEN (Assert ⌜app(f; t) ∈ {G.𝕀, (phi)p ⊢ _:A}⌝⋅
         THENA ((Assert ⌜f ∈ {G.𝕀, (phi)p ⊢ _:(T ⟶ A)}⌝⋅ THENA Auto)
                THEN CubicalAppFun⋅
                THEN RWW "cubical-fun-subset" 0
                THEN Auto)
         )
   THEN (InstLemma `comp_term_wf` [⌜G⌝;⌜phi⌝;⌜A⌝;⌜cA⌝]⋅ THENA Auto)
   THEN Folds ``partial-term-0 partial-term-1`` (-1)
   THEN InstHyp [⌜app(f; t)⌝;⌜app((f)[0(𝕀)]; t0)⌝] (-1)⋅
   THEN Try (Trivial)
   THEN ThinVar `cA') }

1
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G.𝕀 ⊢ _}
4. T : {G.𝕀 ⊢ _}
5. f : {G.𝕀 ⊢ _:(T ⟶ A)}
6. t : {G.𝕀, (phi)p ⊢ _:T}
7. t0 : {G ⊢ _:(T)[0(𝕀)][phi |⟶ t[0]]}
8. app(f; t) ∈ {G.𝕀, (phi)p ⊢ _:A}
⊢ app(f; t) ∈ {G, phi.𝕀 ⊢ _:A}

2
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G.𝕀 ⊢ _}
4. T : {G.𝕀 ⊢ _}
5. f : {G.𝕀 ⊢ _:(T ⟶ A)}
6. t : {G.𝕀, (phi)p ⊢ _:T}
7. t0 : {G ⊢ _:(T)[0(𝕀)][phi |⟶ t[0]]}
8. app(f; t) ∈ {G.𝕀, (phi)p ⊢ _:A}
⊢ app((f)[0(𝕀)]; t0) ∈ {G ⊢ _:(A)[0(𝕀)][phi |⟶ app(f; t)[0]]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[phi:\{G  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A,T:\{G.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[f:\{G.\mBbbI{}  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}].  \mforall{}[t:\{G.\mBbbI{},  (phi)p  \mvdash{}  \_:T\}].
\mforall{}[t0:\{G  \mvdash{}  \_:(T)[0(\mBbbI{})][phi  |{}\mrightarrow{}  t[0]]\}].  \mforall{}[cA:composition-function\{j:l,i:l\}(G.\mBbbI{};A)].
    (pres-c1(G;phi;f;t;t0;cA)  \mmember{}  \{G  \mvdash{}  \_:(A)[1(\mBbbI{})][phi  |{}\mrightarrow{}  app(f;  t)[1]]\})


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  Unfold  `pres-c1`  0
  THEN  (Assert  \mkleeneopen{}app(f;  t)  \mmember{}  \{G.\mBbbI{},  (phi)p  \mvdash{}  \_:A\}\mkleeneclose{}\mcdot{}
              THENA  ((Assert  \mkleeneopen{}f  \mmember{}  \{G.\mBbbI{},  (phi)p  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  CubicalAppFun\mcdot{}
                            THEN  RWW  "cubical-fun-subset"  0
                            THEN  Auto)
              )
  THEN  (InstLemma  `comp\_term\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}cA\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Folds  ``partial-term-0  partial-term-1``  (-1)
  THEN  InstHyp  [\mkleeneopen{}app(f;  t)\mkleeneclose{};\mkleeneopen{}app((f)[0(\mBbbI{})];  t0)\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Try  (Trivial)
  THEN  ThinVar  `cA')

---

Home Index