---

Step * of Lemma pcorec-ext

∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)].
  pcorec(lbl,p.a[lbl;p]) ≡ ptuple(lbl,p.a[lbl;p];pcorec(lbl,p.a[lbl;p]))
BY
{ (Auto
   THEN Unfold `pcorec` 0
   THEN ((InstLemma `corec-family-ext` [⌜P⌝;⌜λX.ptuple(lbl,p.a[lbl;p];X)⌝]⋅ THENM (Reduce -1 THEN Auto)) THENA Auto)) }

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[a:Atom  {}\mrightarrow{}  P  {}\mrightarrow{}  ((P  +  P  +  Type)  List)].
    pcorec(lbl,p.a[lbl;p])  \mequiv{}  ptuple(lbl,p.a[lbl;p];pcorec(lbl,p.a[lbl;p]))


By

---

Latex:
(Auto
  THEN  Unfold  `pcorec`  0
  THEN  ((InstLemma  `corec-family-ext`  [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}\mlambda{}X.ptuple(lbl,p.a[lbl;p];X)\mkleeneclose{}]\mcdot{}
              THENM  (Reduce  -1  THEN  Auto)
              )
              THENA  Auto
              ))

---

Home Index