---

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

No Annotations
∀[I,K:Cname List]. ∀[i:ℕ2]. ∀[f:name-morph(I;K)].
  (((fresh-cname(I):=i) o f) = ((f)+ o (fresh-cname(K):=i)) ∈ name-morph(I+;K))
BY
{ (Auto
   THEN BLemma `name-morphs-equal`
   THEN Auto
   THEN (RepUR ``name-comp name-morph-extend`` 0 THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto)))
   THEN Fold `eq-cname` 0
   THEN RepUR ``compose`` 0
   THEN EqCD
   THEN Auto
   THEN AutoSplit) }

1
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)

2
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)) (f x)) ∈ extd-nameset(K)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I,K:Cname  List].  \mforall{}[i:\mBbbN{}2].  \mforall{}[f:name-morph(I;K)].
    (((fresh-cname(I):=i)  o  f)  =  ((f)+  o  (fresh-cname(K):=i)))


By

---

Latex:
(Auto
  THEN  BLemma  `name-morphs-equal`
  THEN  Auto
  THEN  (RepUR  ``name-comp  name-morph-extend``  0  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))
  THEN  Fold  `eq-cname`  0
  THEN  RepUR  ``compose``  0
  THEN  EqCD
  THEN  Auto
  THEN  AutoSplit)

---

Home Index