---

Step * of Lemma assert-union-deq

∀[A,B:Type]. ∀[a:EqDecider(A)]. ∀[b:EqDecider(B)]. ∀[x,y:A + B].  uiff(↑(union-deq(A;B;a;b) x y);x = y ∈ (A + B))
BY
{ ((UnivCD THENA Auto) THEN RWO "assert-deq" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[a:EqDecider(A)].  \mforall{}[b:EqDecider(B)].  \mforall{}[x,y:A  +  B].
    uiff(\muparrow{}(union-deq(A;B;a;b)  x  y);x  =  y)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RWO  "assert-deq"  0  THEN  Auto)

---

Home Index