---

Step * 1 1 1 1 1 of Lemma cubical-refl_wf


1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. I : Cname List
5. J : Cname List
6. f : name-morph(I;J)
7. alpha : X(I)
8. v : {x:Cname| ¬(x ∈ I)} 
9. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)} 
10. v1 : {x:Cname| ¬(x ∈ J)} 
11. fresh-cname(J) = v1 ∈ {x:Cname| ¬(x ∈ J)} 
⊢ rename-one-name(v1;v1) = 1 ∈ name-morph([v1 / J];[v1 / J])
BY
{ (DSetVars THEN (InstLemma `rename-one-same` [⌜J⌝]⋅ THENA Auto) THEN RWO "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  a  :  \{X  \mvdash{}  \_:A\}
4.  I  :  Cname  List
5.  J  :  Cname  List
6.  f  :  name-morph(I;J)
7.  alpha  :  X(I)
8.  v  :  \{x:Cname|  \mneg{}(x  \mmember{}  I)\} 
9.  fresh-cname(I)  =  v
10.  v1  :  \{x:Cname|  \mneg{}(x  \mmember{}  J)\} 
11.  fresh-cname(J)  =  v1
\mvdash{}  rename-one-name(v1;v1)  =  1


By

---

Latex:
(DSetVars  THEN  (InstLemma  `rename-one-same`  [\mkleeneopen{}J\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RWO  "-1"  0  THEN  Auto)

---

Home Index