---

Step * 1 of Lemma Q-R-glues_wf


1. Info : Type
2. es : EO+(Info)
3. Qa : E ⟶ E ⟶ ℙ
4. Rb : E ⟶ E ⟶ ℙ
5. A : Type
6. B : Type
7. Ia : EClass(A)
8. Ib : EClass(B)
9. f : E(Ia) ⟶ B
10. g : E(Ib) ⟶ E
11. {Ia} ←←= g== {Ib}
12. g is Qa-Rb-pre-preserving on {Ib}
13. Inj(E(Ib);E;g)
14. e : E(Ib)@i
⊢ g e ∈ E(Ia)
BY
{ OnMaybeHyp 11 (\h. (D h
                      THEN RepUR ``weak-antecedent-function es-interface-predicate`` h
                      THEN MemTypeCD
                      THEN Complete (Auto))) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  Qa  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
4.  Rb  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
5.  A  :  Type
6.  B  :  Type
7.  Ia  :  EClass(A)
8.  Ib  :  EClass(B)
9.  f  :  E(Ia)  {}\mrightarrow{}  B
10.  g  :  E(Ib)  {}\mrightarrow{}  E
11.  \{Ia\}  \mleftarrow{}\mleftarrow{}=  g==  \{Ib\}
12.  g  is  Qa-Rb-pre-preserving  on  \{Ib\}
13.  Inj(E(Ib);E;g)
14.  e  :  E(Ib)@i
\mvdash{}  g  e  \mmember{}  E(Ia)


By

---

Latex:
OnMaybeHyp  11  (\mbackslash{}h.  (D  h
                                        THEN  RepUR  ``weak-antecedent-function  es-interface-predicate``  h
                                        THEN  MemTypeCD
                                        THEN  Complete  (Auto)))

---

Home Index