---

Step * 3 1 2 1 2 1 of Lemma cu-filler-cases


1. I : Cname List
2. J : nameset(I) List
3. K : Cname List
4. x : Cname
5. (x ∈ I)
6. f : name-morph(I-[x];K)
7. i : ℕ2
8. box : open_box(c𝕌;I;J;x;i)
9. J ∈ nameset(J) List
10. nameset(J) ⊆r nameset(I-[x])
11. y : (∀y∈J.¬↑¬bisname(f y))
12. l-first(y.¬bisname(f y);J) = (inr y ) ∈ ((∃y:nameset(J) [((y ∈ J) ∧ (↑¬bisname(f y)))]) ∨ (∀y∈J.¬↑¬bisname(f y)))
13. (∀y∈J.¬↑¬bisname(f y)) ∧ True
14. f[x:=fresh-cname(K)] ∈ name-morph(I;[fresh-cname(K) / K])
15. x1 : Cname
16. (x1 = x ∈ Cname) ∨ (x1 ∈ J)
⊢ x1 ∈ nameset(I)
BY
{ TACTIC:(D -1 THEN Try ((HypSubst' (-1) 0 THEN Auto))) }

1
1. I : Cname List
2. J : nameset(I) List
3. K : Cname List
4. x : Cname
5. (x ∈ I)
6. f : name-morph(I-[x];K)
7. i : ℕ2
8. box : open_box(c𝕌;I;J;x;i)
9. J ∈ nameset(J) List
10. nameset(J) ⊆r nameset(I-[x])
11. y : (∀y∈J.¬↑¬bisname(f y))
12. l-first(y.¬bisname(f y);J) = (inr y ) ∈ ((∃y:nameset(J) [((y ∈ J) ∧ (↑¬bisname(f y)))]) ∨ (∀y∈J.¬↑¬bisname(f y)))
13. (∀y∈J.¬↑¬bisname(f y)) ∧ True
14. f[x:=fresh-cname(K)] ∈ name-morph(I;[fresh-cname(K) / K])
15. x1 : Cname
16. (x1 ∈ J)
⊢ x1 ∈ nameset(I)

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  J  :  nameset(I)  List
3.  K  :  Cname  List
4.  x  :  Cname
5.  (x  \mmember{}  I)
6.  f  :  name-morph(I-[x];K)
7.  i  :  \mBbbN{}2
8.  box  :  open\_box(c\mBbbU{};I;J;x;i)
9.  J  \mmember{}  nameset(J)  List
10.  nameset(J)  \msubseteq{}r  nameset(I-[x])
11.  y  :  (\mforall{}y\mmember{}J.\mneg{}\muparrow{}\mneg{}\msubb{}isname(f  y))
12.  l-first(y.\mneg{}\msubb{}isname(f  y);J)  =  (inr  y  )
13.  (\mforall{}y\mmember{}J.\mneg{}\muparrow{}\mneg{}\msubb{}isname(f  y))  \mwedge{}  True
14.  f[x:=fresh-cname(K)]  \mmember{}  name-morph(I;[fresh-cname(K)  /  K])
15.  x1  :  Cname
16.  (x1  =  x)  \mvee{}  (x1  \mmember{}  J)
\mvdash{}  x1  \mmember{}  nameset(I)


By

---

Latex:
TACTIC:(D  -1  THEN  Try  ((HypSubst'  (-1)  0  THEN  Auto)))

---

Home Index