---

Step * 1 of Lemma face-forall-implies


1. H : CubicalSet{j}
2. phi : {H.𝕀 ⊢ _:𝔽}
3. p ∈ H.𝕀 j⟶ H
4. I : fset(ℕ)
5. alpha : H(I)
6. x : Point(dM(I))
7. ((∀ phi))p(<alpha, x>) = 1 ∈ Point(face_lattice(I))
8. (new-name(I)/x) ∈ I ⟶ I+new-name(I)
9. <new-name(I)> ∈ 𝕀(s(alpha))
⊢ phi(<alpha, x>) = 1 ∈ Point(face_lattice(I))
BY
{ (Assert ⌜(phi(<s(alpha), <new-name(I)>>))<(new-name(I)/x)> = phi(<alpha, x>) ∈ Point(face_lattice(I))⌝⋅
   THENA ((InstLemma `cubical-term-at-morph` [⌜H.𝕀⌝;⌜𝔽⌝;⌜phi⌝;⌜I+new-name(I)⌝;⌜(s(alpha);<new-name(I)>)⌝;⌜I⌝;
           ⌜(new-name(I)/x)⌝]⋅
           THENA Auto
           )
          THEN (RWO "face-type-at" (-1) THENA Auto)
          THEN (RWO "face-type-ap-morph" (-1) THENA Auto)
          THEN RepUR ``cube-context-adjoin cc-adjoin-cube`` -1
          THEN NthHypEq (-1)
          THEN EqCDA)
   ) }

1
.....subterm..... T:t
3:n
1. H : CubicalSet{j}
2. phi : {H.𝕀 ⊢ _:𝔽}
3. p ∈ H.𝕀 j⟶ H
4. I : fset(ℕ)
5. alpha : H(I)
6. x : Point(dM(I))
7. ((∀ phi))p(<alpha, x>) = 1 ∈ Point(face_lattice(I))
8. (new-name(I)/x) ∈ I ⟶ I+new-name(I)
9. <new-name(I)> ∈ 𝕀(s(alpha))
10. (phi(<s(alpha), <new-name(I)>>))<(new-name(I)/x)>
= phi(<(new-name(I)/x)(s(alpha)), (<new-name(I)> s(alpha) (new-name(I)/x))>)
∈ Point(face_lattice(I))
⊢ phi(<alpha, x>) = phi(<(new-name(I)/x)(s(alpha)), (<new-name(I)> s(alpha) (new-name(I)/x))>) ∈ Point(face_lattice(I))

2
1. H : CubicalSet{j}
2. phi : {H.𝕀 ⊢ _:𝔽}
3. p ∈ H.𝕀 j⟶ H
4. I : fset(ℕ)
5. alpha : H(I)
6. x : Point(dM(I))
7. ((∀ phi))p(<alpha, x>) = 1 ∈ Point(face_lattice(I))
8. (new-name(I)/x) ∈ I ⟶ I+new-name(I)
9. <new-name(I)> ∈ 𝕀(s(alpha))
10. (phi(<s(alpha), <new-name(I)>>))<(new-name(I)/x)> = phi(<alpha, x>) ∈ Point(face_lattice(I))
⊢ phi(<alpha, x>) = 1 ∈ Point(face_lattice(I))

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
2.  phi  :  \{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}
3.  p  \mmember{}  H.\mBbbI{}  j{}\mrightarrow{}  H
4.  I  :  fset(\mBbbN{})
5.  alpha  :  H(I)
6.  x  :  Point(dM(I))
7.  ((\mforall{}  phi))p(<alpha,  x>)  =  1
8.  (new-name(I)/x)  \mmember{}  I  {}\mrightarrow{}  I+new-name(I)
9.  <new-name(I)>  \mmember{}  \mBbbI{}(s(alpha))
\mvdash{}  phi(<alpha,  x>)  =  1


By

---

Latex:
(Assert  \mkleeneopen{}(phi(<s(alpha),  <new-name(I)>>))<(new-name(I)/x)>  =  phi(<alpha,  x>)\mkleeneclose{}\mcdot{}
  THENA  ((InstLemma  `cubical-term-at-morph`  [\mkleeneopen{}H.\mBbbI{}\mkleeneclose{};\mkleeneopen{}\mBbbF{}\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}I+new-name(I)\mkleeneclose{};
                  \mkleeneopen{}(s(alpha);<new-name(I)>)\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}(new-name(I)/x)\mkleeneclose{}]\mcdot{}
                  THENA  Auto
                  )
                THEN  (RWO  "face-type-at"  (-1)  THENA  Auto)
                THEN  (RWO  "face-type-ap-morph"  (-1)  THENA  Auto)
                THEN  RepUR  ``cube-context-adjoin  cc-adjoin-cube``  -1
                THEN  NthHypEq  (-1)
                THEN  EqCDA)
  )

---

Home Index