---

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:


\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

Auto

---

Home Index