---

Step * 1 1 1 of Lemma msg-rename_wf


1. M : IdLnk ─→ Id ─→ Type
2. rt : Id ─→ Id
3. rtinv : Id ─→ (Id?)
4. inv-rel(Id;Id;rt;rtinv)
5. l : IdLnk
6. t : Id
7. m2 : M l t
8. ↑isl(rtinv t)
⊢ m2 ∈ M l (rt outl(rtinv t))
BY
{ (Subst' ⌈(rt outl(rtinv t)) = t ∈ Id⌉ 0⋅ THEN Auto) }

1
.....equality..... 
1. M : IdLnk ─→ Id ─→ Type
2. rt : Id ─→ Id
3. rtinv : Id ─→ (Id?)
4. inv-rel(Id;Id;rt;rtinv)
5. l : IdLnk
6. t : Id
7. m2 : M l t
8. ↑isl(rtinv t)
⊢ (rt outl(rtinv t)) = t ∈ Id

---

Latex:



1.  M  :  IdLnk  {}\mrightarrow{}  Id  {}\mrightarrow{}  Type
2.  rt  :  Id  {}\mrightarrow{}  Id
3.  rtinv  :  Id  {}\mrightarrow{}  (Id?)
4.  inv-rel(Id;Id;rt;rtinv)
5.  l  :  IdLnk
6.  t  :  Id
7.  m2  :  M  l  t
8.  \muparrow{}isl(rtinv  t)
\mvdash{}  m2  \mmember{}  M  l  (rt  outl(rtinv  t))


By

(Subst'  \mkleeneopen{}(rt  outl(rtinv  t))  =  t\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index