---

Step * of Lemma name-morph-extend_wf

∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  ((f)+ ∈ name-morph(I+;J+))
BY
{ (Auto
   THEN Unfolds ``add-fresh-cname name-morph-extend`` 0
   THEN GenConclTerms Auto [⌜fresh-cname(I)⌝;⌜fresh-cname(J)⌝]⋅
   THEN DSetVars
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))) }

1
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. v : Cname
5. ¬(v ∈ I)
6. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)} 
7. v1 : Cname
8. ¬(v1 ∈ J)
9. fresh-cname(J) = v1 ∈ {x:Cname| ¬(x ∈ J)} 
⊢ λx.if CnameDeq x v then v1 else f x fi  ∈ name-morph([v / I];[v1 / J])

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Unfolds  ``add-fresh-cname  name-morph-extend``  0
  THEN  GenConclTerms  Auto  [\mkleeneopen{}fresh-cname(I)\mkleeneclose{};\mkleeneopen{}fresh-cname(J)\mkleeneclose{}]\mcdot{}
  THEN  DSetVars
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))

---

Home Index