---

Step * of Lemma Q-Q-glued-self-image

∀[Info:Type]. ∀es:EO+(Info). ∀[A,B:Type].  ∀Ia:EClass(A). ∀f:A ─→ B.  ∀[Q:E ─→ E ─→ ℙ]. Ia:Q →─λe.(f Ia(e))─→  f'Ia:Q
BY
{ (Auto THEN Unfold `Q-R-glued` 0) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. [A] : Type
4. [B] : Type
5. Ia : EClass(A)@i'
6. f : A ─→ B@i
7. [Q] : E ─→ E ─→ ℙ
⊢ ∃g:E(f'Ia) ─→ E. g glues Ia:Q ──λe.(f Ia(e))─→ f'Ia:Q

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[A,B:Type].    \mforall{}Ia:EClass(A).  \mforall{}f:A  {}\mrightarrow{}  B.    \mforall{}[Q:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  Ia:Q  \mrightarrow{}{}\mlambda{}e.(f  Ia(e)){}\mrightarrow{}    f'Ia:Q


By

---

Latex:
(Auto  THEN  Unfold  `Q-R-glued`  0)

---

Home Index