Step
*
1
1
1
of Lemma
lift-id-face_wf
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. alpha : X(I)
7. x : nameset(I)
8. i : ℕ2
9. w : (Id_A a b)((x:=i)(alpha))
10. x = fresh-cname(I) ∈ Cname
⊢ [fresh-cname(I) / I-[x]] = I-[x] ∈ (Cname List)
BY
{ TACTIC:DVar `x' }
1
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. alpha : X(I)
7. x : Cname
8. (x ∈ I)
9. i : ℕ2
10. w : (Id_A a b)((x:=i)(alpha))
11. x = fresh-cname(I) ∈ Cname
⊢ [fresh-cname(I) / I-[x]] = I-[x] ∈ (Cname List)
Latex:
Latex:
1. X : CubicalSet
2. A : \{X \mvdash{} \_\}
3. a : \{X \mvdash{} \_:A\}
4. b : \{X \mvdash{} \_:A\}
5. I : Cname List
6. alpha : X(I)
7. x : nameset(I)
8. i : \mBbbN{}2
9. w : (Id\_A a b)((x:=i)(alpha))
10. x = fresh-cname(I)
\mvdash{} [fresh-cname(I) / I-[x]] = I-[x]
By
Latex:
TACTIC:DVar `x'
Home
Index