---

Step * of Lemma conditional_wf-interface

∀[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([Ia1?Ia2]))
BY
{ ((UnivCD THENA Auto) THEN Unfold `conditional` 0) }

1
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. Ia1 : EClass(A)
6. Ia2 : EClass(A)
7. Ib1 : EClass(B)
8. Ib2 : EClass(B)
9. g1 : E(Ib1) ─→ E(Ia1)
10. g2 : E(Ib2) ─→ E(Ia2)
⊢ λx.if p:{Ib1} x then g1 x else g2 x fi  ∈ E([Ib1?Ib2]) ─→ E([Ia1?Ia2])

---

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([Ia1?Ia2]))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `conditional`  0)

---

Home Index