---

Step * 1 1 1 1 of Lemma msg-rename_wf

.....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
BY
{ (Symmetry
   THEN (((MoveToConcl (-1)) THEN (GenConclAtAddr [1; 1; 1])) THENA Auto)
   THEN (D (-2))
   THEN Reduce 0
   THEN Auto) }

---

Latex:


.....equality..... 
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{}  (rt  outl(rtinv  t))  =  t


By

(Symmetry
  THEN  (((MoveToConcl  (-1))  THEN  (GenConclAtAddr  [1;  1;  1]))  THENA  Auto)
  THEN  (D  (-2))
  THEN  Reduce  0
  THEN  Auto)

---

Home Index