---

Step * 1 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
⊢ x ∈ E(Ib2)
BY
{ (D -2 THEN (RWO "is-cond-class" (-2) THENM D -2) THEN Auto)⋅ }

---

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{}  x  \mmember{}  E(Ib2)


By

---

Latex:
(D  -2  THEN  (RWO  "is-cond-class"  (-2)  THENM  D  -2)  THEN  Auto)\mcdot{}

---

Home Index