---

Step * of Lemma csm-rev_fill_term

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 ⊢ Compositon(A)]. ∀[u:{Gamma.𝕀, (phi)p ⊢ _:A}].
∀[a1:{Gamma ⊢ _:(A)[1(𝕀)][phi |⟶ u[1]]}]. ∀[Delta:j⊢]. ∀[s:Delta j⟶ Gamma].
  ((rev_fill_term(Gamma;cA;phi;u;a1))s+
  = rev_fill_term(Delta;(cA)s+;(phi)s;(u)s+;(a1)s)
  ∈ {Delta.𝕀 ⊢ _:(A)s+[((phi)s)p |⟶ (u)s+]})
BY
{ ((Intros THEN (Assert 1-(q) ∈ {Gamma.𝕀 ⊢ _:(𝕀)p} BY (SubsumeC ⌜{Gamma.𝕀 ⊢ _:𝕀}⌝⋅ THEN Auto)))
   THEN (InstLemma `csm-constrained-cubical-term` [⌜Gamma.𝕀⌝;⌜Delta.𝕀⌝;⌜s+⌝;⌜A⌝;⌜(phi)p⌝;⌜u⌝;
         ⌜rev_fill_term(Gamma;cA;phi;u;a1)⌝]⋅
         THENA Auto
         )
   ) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. cA : Gamma.𝕀 ⊢ Compositon(A)
5. u : {Gamma.𝕀, (phi)p ⊢ _:A}
6. a1 : {Gamma ⊢ _:(A)[1(𝕀)][phi |⟶ u[1]]}
7. Delta : CubicalSet{j}
8. s : Delta j⟶ Gamma
9. 1-(q) ∈ {Gamma.𝕀 ⊢ _:(𝕀)p}
10. (rev_fill_term(Gamma;cA;phi;u;a1))s+ ∈ {Delta.𝕀 ⊢ _:(A)s+[((phi)p)s+ |⟶ (u)s+]}
⊢ (rev_fill_term(Gamma;cA;phi;u;a1))s+
= rev_fill_term(Delta;(cA)s+;(phi)s;(u)s+;(a1)s)
∈ {Delta.𝕀 ⊢ _:(A)s+[((phi)s)p |⟶ (u)s+]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{Gamma.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[cA:Gamma.\mBbbI{}  \mvdash{}  Compositon(A)].
\mforall{}[u:\{Gamma.\mBbbI{},  (phi)p  \mvdash{}  \_:A\}].  \mforall{}[a1:\{Gamma  \mvdash{}  \_:(A)[1(\mBbbI{})][phi  |{}\mrightarrow{}  u[1]]\}].  \mforall{}[Delta:j\mvdash{}].
\mforall{}[s:Delta  j{}\mrightarrow{}  Gamma].
    ((rev\_fill\_term(Gamma;cA;phi;u;a1))s+  =  rev\_fill\_term(Delta;(cA)s+;(phi)s;(u)s+;(a1)s))


By

---

Latex:
((Intros  THEN  (Assert  1-(q)  \mmember{}  \{Gamma.\mBbbI{}  \mvdash{}  \_:(\mBbbI{})p\}  BY  (SubsumeC  \mkleeneopen{}\{Gamma.\mBbbI{}  \mvdash{}  \_:\mBbbI{}\}\mkleeneclose{}\mcdot{}  THEN  Auto)))
  THEN  (InstLemma  `csm-constrained-cubical-term`  [\mkleeneopen{}Gamma.\mBbbI{}\mkleeneclose{};\mkleeneopen{}Delta.\mBbbI{}\mkleeneclose{};\mkleeneopen{}s+\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}(phi)p\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};
              \mkleeneopen{}rev\_fill\_term(Gamma;cA;phi;u;a1)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  )

---

Home Index