---

Step * of Lemma union-deq_wf

∀[A,B:Type]. ∀[a:EqDecider(A)]. ∀[b:EqDecider(B)].  (union-deq(A;B;a;b) ∈ EqDecider(A + B))
BY
{ (Auto
   THEN Unfold `union-deq` 0
   THEN Unfold `deq` 0
   THEN MemTypeCD
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN (UnivCD THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[a:EqDecider(A)].  \mforall{}[b:EqDecider(B)].    (union-deq(A;B;a;b)  \mmember{}  EqDecider(A  +  B))


By

---

Latex:
(Auto
  THEN  Unfold  `union-deq`  0
  THEN  Unfold  `deq`  0
  THEN  MemTypeCD
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  (UnivCD  THENA  Auto))

---

Home Index