---

Step * 1 1 of Lemma conditional_wf-interface


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)
11. x : E([Ib1?Ib2])@i
12. q : ¬↑x ∈b Ib1
⊢ g2 x ∈ E([Ia1?Ia2])
BY
{ Auto }

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)
11. x : E([Ib1?Ib2])@i
12. q : ¬↑x ∈b Ib1
⊢ x ∈ E(Ib2)

---

Latex:

---

Latex:

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)  {}\mrightarrow{}  E(Ia1)
10.  g2  :  E(Ib2)  {}\mrightarrow{}  E(Ia2)
11.  x  :  E([Ib1?Ib2])@i
12.  q  :  \mneg{}\muparrow{}x  \mmember{}\msubb{}  Ib1
\mvdash{}  g2  x  \mmember{}  E([Ia1?Ia2])


By

---

Latex:
Auto

---

Home Index