---

Step * of Lemma mtype-sqequal

∀[L:MutualRectypeSpec]. ∀[i:mKinds].  (mtype(L;i) ~ mrec(L;i))
BY
{ (Auto
   THEN Unfold `mtype` 0
   THEN (InstLemma `apply_alist-eager-map-atom` [⌜parm{i'}⌝;⌜Atom × ((Atom × ((Atom + Atom + Type) List)) List)⌝;⌜L⌝;
         ⌜λp.(fst(p))⌝;⌜λi.mrec(L;i)⌝;⌜i⌝]⋅
         THENA Auto
         )
   THEN Reduce -1
   THEN NthHypSq (-1)
   THEN RepeatFor 2 ((EqCD THEN Try (Trivial)))
   THEN All Thin) }

1
1. L : MutualRectypeSpec
⊢ eager-map(λp.let i,x = p 
               in <i, mrec(L;i)>;L) ~ eager-map(λa.<fst(a), mrec(L;fst(a))>;L)

---

Latex:

---

Latex:
\mforall{}[L:MutualRectypeSpec].  \mforall{}[i:mKinds].    (mtype(L;i)  \msim{}  mrec(L;i))


By

---

Latex:
(Auto
  THEN  Unfold  `mtype`  0
  THEN  (InstLemma  `apply\_alist-eager-map-atom`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};
              \mkleeneopen{}Atom  \mtimes{}  ((Atom  \mtimes{}  ((Atom  +  Atom  +  Type)  List))  List)\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}\mlambda{}p.(fst(p))\mkleeneclose{};\mkleeneopen{}\mlambda{}i.mrec(L;i)\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Reduce  -1
  THEN  NthHypSq  (-1)
  THEN  RepeatFor  2  ((EqCD  THEN  Try  (Trivial)))
  THEN  All  Thin)

---

Home Index