---

Step * 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
⊢ x = y ∈ (A + B) ⇐⇒ ↑(sumdeq(a;b) x y)
BY
{ ((Assert ∀x,y:A.  (x = y ∈ A ⇐⇒ ↑(a x y)) BY
          (DVar `a' THEN Unhide THEN Auto))
   THEN (Assert ∀x,y:B.  (x = y ∈ B ⇐⇒ ↑(b x y)) BY
               (DVar `b' THEN Unhide THEN Auto))
   ) }

1
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)

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  \mforall{}x,y:A.    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(a  x  y))  BY
                (DVar  `a'  THEN  Unhide  THEN  Auto))
  THEN  (Assert  \mforall{}x,y:B.    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(b  x  y))  BY
                          (DVar  `b'  THEN  Unhide  THEN  Auto))
  )

---

Home Index