---

Step * 1 1 1 of Lemma cubical-id-box_wf

.....assertion..... 
1. c : ℕ2
2. I : Cname List
3. X : CubicalSet
4. A : {X ⊢ _}
5. a : {X ⊢ _:A}
6. b : {X ⊢ _:A}
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. alpha : X(I)
11. ¬(fresh-cname(I) ∈ J)
12. ¬(x = fresh-cname(I) ∈ Cname)
13. v : {x:Cname| ¬(x ∈ I)} 
14. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)} 
15. x1 : nameset(I)
16. i1 : ℕ2
17. ¬(fresh-cname(I) = x1 ∈ Cname)
18. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
19. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha)) ∈ A((x1:=i1)(alpha))
⊢ [fresh-cname(I) / I]-[x1] = [fresh-cname(I) / I-[x1]] ∈ (Cname List)
BY
{ TACTIC:((GenConclTerm ⌜fresh-cname(I)⌝⋅ THENA Auto) THEN (Assert ¬(v3 ∈ [x1]) BY (D 0 THENA Auto))) }

1
.....aux..... 
1. c : ℕ2
2. I : Cname List
3. X : CubicalSet
4. A : {X ⊢ _}
5. a : {X ⊢ _:A}
6. b : {X ⊢ _:A}
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. alpha : X(I)
11. ¬(fresh-cname(I) ∈ J)
12. ¬(x = fresh-cname(I) ∈ Cname)
13. v : {x:Cname| ¬(x ∈ I)} 
14. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)} 
15. x1 : nameset(I)
16. i1 : ℕ2
17. ¬(fresh-cname(I) = x1 ∈ Cname)
18. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
19. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha)) ∈ A((x1:=i1)(alpha))
20. v3 : {x:Cname| ¬(x ∈ I)} 
21. fresh-cname(I) = v3 ∈ {x:Cname| ¬(x ∈ I)} 
22. (v3 ∈ [x1])
⊢ False

2
1. c : ℕ2
2. I : Cname List
3. X : CubicalSet
4. A : {X ⊢ _}
5. a : {X ⊢ _:A}
6. b : {X ⊢ _:A}
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. alpha : X(I)
11. ¬(fresh-cname(I) ∈ J)
12. ¬(x = fresh-cname(I) ∈ Cname)
13. v : {x:Cname| ¬(x ∈ I)} 
14. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)} 
15. x1 : nameset(I)
16. i1 : ℕ2
17. ¬(fresh-cname(I) = x1 ∈ Cname)
18. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
19. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha)) ∈ A((x1:=i1)(alpha))
20. v3 : {x:Cname| ¬(x ∈ I)} 
21. fresh-cname(I) = v3 ∈ {x:Cname| ¬(x ∈ I)} 
22. ¬(v3 ∈ [x1])
⊢ [v3 / I]-[x1] = [v3 / I-[x1]] ∈ (Cname List)

---

Latex:

---

Latex:
.....assertion..... 
1.  c  :  \mBbbN{}2
2.  I  :  Cname  List
3.  X  :  CubicalSet
4.  A  :  \{X  \mvdash{}  \_\}
5.  a  :  \{X  \mvdash{}  \_:A\}
6.  b  :  \{X  \mvdash{}  \_:A\}
7.  J  :  nameset(I)  List
8.  x  :  nameset(I)
9.  i  :  \mBbbN{}2
10.  alpha  :  X(I)
11.  \mneg{}(fresh-cname(I)  \mmember{}  J)
12.  \mneg{}(x  =  fresh-cname(I))
13.  v  :  \{x:Cname|  \mneg{}(x  \mmember{}  I)\} 
14.  fresh-cname(I)  =  v
15.  x1  :  nameset(I)
16.  i1  :  \mBbbN{}2
17.  \mneg{}(fresh-cname(I)  =  x1)
18.  v2  :  A(iota(fresh-cname(I))((x1:=i1)(alpha)))
19.  (v2  iota(fresh-cname(I))((x1:=i1)(alpha))  (fresh-cname(I):=c))  =  (a  I-[x1]  (x1:=i1)(alpha))
\mvdash{}  [fresh-cname(I)  /  I]-[x1]  =  [fresh-cname(I)  /  I-[x1]]


By

---

Latex:
TACTIC:((GenConclTerm  \mkleeneopen{}fresh-cname(I)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (Assert  \mneg{}(v3  \mmember{}  [x1])  BY  (D  0  THENA  Auto)))

---

Home Index