---

Step * 2 of Lemma disjoint-quotient_subtype


1. A : Type
2. B : Type
3. ¬(A ∧ B)
4. E : (A + B) ⟶ (A + B) ⟶ ℙ
5. EquivRel(A + B;x,y.E[x;y])
6. EquivRel(A;x,y.E[inl x;inl y])
7. EquivRel(B;x,y.E[inr x ;inr y ])
8. x1 : A
9. y : B
10. E[inl x1;inr y ]
⊢ (inl x1) = (inr y ) ∈ (a1,a2:A//E[inl a1;inl a2] + (b1,b2:B//E[inr b1 ;inr b2 ]))
BY
{ (D 3 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  \mneg{}(A  \mwedge{}  B)
4.  E  :  (A  +  B)  {}\mrightarrow{}  (A  +  B)  {}\mrightarrow{}  \mBbbP{}
5.  EquivRel(A  +  B;x,y.E[x;y])
6.  EquivRel(A;x,y.E[inl  x;inl  y])
7.  EquivRel(B;x,y.E[inr  x  ;inr  y  ])
8.  x1  :  A
9.  y  :  B
10.  E[inl  x1;inr  y  ]
\mvdash{}  (inl  x1)  =  (inr  y  )


By

---

Latex:
(D  3  THEN  Auto)

---

Home Index