---

Step * of Lemma conditional_wf-interface2

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:Type]. ∀[Ia1,Ia2:EClass(A)]. ∀[Ib1,Ib2:EClass(B)]. ∀[g1:E(Ib1) ⟶ E(Ia1)].
∀[g2:E(Ib2) ⟶ E(Ia2)].
  ([{Ib1}? g1 : g2] ∈ E([Ib1?Ib2]) ⟶ E)
BY
{ ((UnivCD THENA Auto) THEN SubsumeC ⌜E([Ib1?Ib2]) ⟶ E([Ia1?Ia2])⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,B:Type].  \mforall{}[Ia1,Ia2:EClass(A)].  \mforall{}[Ib1,Ib2:EClass(B)].
\mforall{}[g1:E(Ib1)  {}\mrightarrow{}  E(Ia1)].  \mforall{}[g2:E(Ib2)  {}\mrightarrow{}  E(Ia2)].
    ([\{Ib1\}?  g1  :  g2]  \mmember{}  E([Ib1?Ib2])  {}\mrightarrow{}  E)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  SubsumeC  \mkleeneopen{}E([Ib1?Ib2])  {}\mrightarrow{}  E([Ia1?Ia2])\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index