---

Step * 1 of Lemma name-morph-extend-face-map


1. I : Cname List
2. K : Cname List
3. i : ℕ2
4. f : name-morph(I;K)
5. x : nameset(I+)
6. x = fresh-cname(I) ∈ Cname
⊢ (uext(f) ((fresh-cname(I):=i) x)) = (uext((fresh-cname(K):=i)) fresh-cname(K)) ∈ extd-nameset(K)
BY
{ (HypSubst' (-1) 0
   THEN RepUR ``face-map`` 0
   THEN AutoSplit
   THEN RepUR ``uext`` 0
   THEN (Subst' isname(i) ~ ff 0 THENA (RepUR ``isname`` 0 THEN Auto))
   THEN Reduce 0
   THEN (Subst' isname(fresh-cname(K)) ~ tt 0
         THENA (GenConclTerm ⌜fresh-cname(K)⌝⋅ THEN Auto THEN RepeatFor 2 (DVar `v') THEN RepUR ``isname`` 0 THEN Auto)
         )
   THEN Reduce 0
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  K  :  Cname  List
3.  i  :  \mBbbN{}2
4.  f  :  name-morph(I;K)
5.  x  :  nameset(I+)
6.  x  =  fresh-cname(I)
\mvdash{}  (uext(f)  ((fresh-cname(I):=i)  x))  =  (uext((fresh-cname(K):=i))  fresh-cname(K))


By

---

Latex:
(HypSubst'  (-1)  0
  THEN  RepUR  ``face-map``  0
  THEN  AutoSplit
  THEN  RepUR  ``uext``  0
  THEN  (Subst'  isname(i)  \msim{}  ff  0  THENA  (RepUR  ``isname``  0  THEN  Auto))
  THEN  Reduce  0
  THEN  (Subst'  isname(fresh-cname(K))  \msim{}  tt  0
              THENA  (GenConclTerm  \mkleeneopen{}fresh-cname(K)\mkleeneclose{}\mcdot{}
                            THEN  Auto
                            THEN  RepeatFor  2  (DVar  `v')
                            THEN  RepUR  ``isname``  0
                            THEN  Auto)
              )
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index