---

Step * of Lemma iota'-comp

∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  ((iota'(I) o (f)+) = (f o iota'(J)) ∈ name-morph(I;J+))
BY
{ TACTIC:(Auto
          THEN Symmetry
          THEN BLemma `name-morphs-equal`
          THEN Auto
          THEN RepUR ``iota\' iota name-morph-extend name-comp compose uext`` 0
          THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
          THEN (EqCD THENA Auto)
          THEN Reduce 0) }

1
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. x : nameset(I)
⊢ if isname(f x) then f x else f x fi 
= if isname(x) then if CnameDeq x fresh-cname(I) then fresh-cname(J) else f x fi  else x fi 
∈ extd-nameset(J+)

---

Latex:

---

Latex:
\mforall{}[I,J:Cname  List].  \mforall{}[f:name-morph(I;J)].    ((iota'(I)  o  (f)+)  =  (f  o  iota'(J)))


By

---

Latex:
TACTIC:(Auto
                THEN  Symmetry
                THEN  BLemma  `name-morphs-equal`
                THEN  Auto
                THEN  RepUR  ``iota\mbackslash{}'  iota  name-morph-extend  name-comp  compose  uext``  0
                THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
                THEN  (EqCD  THENA  Auto)
                THEN  Reduce  0)

---

Home Index