---

Step * 1 1 of Lemma union-deq_wf


1. A : Type
2. B : Type
3. a : EqDecider(A)
4. b : EqDecider(B)
5. x : A + B
6. y : A + B
7. ∀x,y:A.  (x = y ∈ A ⇐⇒ ↑(a x y))
8. ∀x,y:B.  (x = y ∈ B ⇐⇒ ↑(b x y))
⊢ x = y ∈ (A + B) ⇐⇒ ↑(sumdeq(a;b) x y)
BY
{ (DVar `x'
   THEN DVar `y'
   THEN RepUR ``sumdeq`` 0
   THEN Auto
   THEN Try ((EqCD THEN Auto))
   THEN ImpossibleUnionEq (-1)⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  a  :  EqDecider(A)
4.  b  :  EqDecider(B)
5.  x  :  A  +  B
6.  y  :  A  +  B
7.  \mforall{}x,y:A.    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(a  x  y))
8.  \mforall{}x,y:B.    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(b  x  y))
\mvdash{}  x  =  y  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(sumdeq(a;b)  x  y)


By

---

Latex:
(DVar  `x'
  THEN  DVar  `y'
  THEN  RepUR  ``sumdeq``  0
  THEN  Auto
  THEN  Try  ((EqCD  THEN  Auto))
  THEN  ImpossibleUnionEq  (-1)\mcdot{}
  THEN  Auto)

---

Home Index