---

Step * of Lemma msg-rename_wf

∀[M:IdLnk ⟶ Id ⟶ Type]. ∀[rt:Id ⟶ Id]. ∀[rtinv:Id ⟶ (Id?)].
  ∀[m:Msg(M)]. msg-rename(rtinv;m) ∈ Msg(λl,tg. (M l (rt tg))) supposing ↑isl(rtinv mtag(m)) 
  supposing inv-rel(Id;Id;rt;rtinv)
BY
{ Auto }

1
1. M : IdLnk ⟶ Id ⟶ Type
2. rt : Id ⟶ Id
3. rtinv : Id ⟶ (Id?)
4. inv-rel(Id;Id;rt;rtinv)
5. m : Msg(M)
6. ↑isl(rtinv mtag(m))
⊢ msg-rename(rtinv;m) ∈ Msg(λl,tg. (M l (rt tg)))

---

Latex:

---

Latex:
\mforall{}[M:IdLnk  {}\mrightarrow{}  Id  {}\mrightarrow{}  Type].  \mforall{}[rt:Id  {}\mrightarrow{}  Id].  \mforall{}[rtinv:Id  {}\mrightarrow{}  (Id?)].
    \mforall{}[m:Msg(M)].  msg-rename(rtinv;m)  \mmember{}  Msg(\mlambda{}l,tg.  (M  l  (rt  tg)))  supposing  \muparrow{}isl(rtinv  mtag(m)) 
    supposing  inv-rel(Id;Id;rt;rtinv)


By

---

Latex:
Auto

---

Home Index