---

Step * of Lemma glued-to-self

∀[Info,A:Type].  ∀es:EO+(Info). ∀v:EClass(A).  glued(es;A;λe.v(e);v;v)
BY
{ (Auto
   THEN ((BLemma `glued-Q-R-glued` THENM BLemma `Q-Q-glued-to-self`) THENA (Auto THEN (D (-1)) THEN Unhide THEN Auto))
   ) }

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].    \mforall{}es:EO+(Info).  \mforall{}v:EClass(A).    glued(es;A;\mlambda{}e.v(e);v;v)


By

---

Latex:
(Auto
  THEN  ((BLemma  `glued-Q-R-glued`  THENM  BLemma  `Q-Q-glued-to-self`)
              THENA  (Auto  THEN  (D  (-1))  THEN  Unhide  THEN  Auto)
              )
  )

---

Home Index