---

Step * of Lemma equipollent-union-com

∀[A,B:Type].  A + B ~ B + A
BY
{ TACTIC:((Auto THEN With ⌜λx.case x of inl(a) => inr a  | inr(b) => inl b⌝ (D 0)⋅)
          THEN Auto
          THEN RepeatFor 2 (D 0)
          THEN Reduce 0
          THEN Auto) }

1
1. A : Type
2. B : Type
3. a1 : A + B@i
4. a2 : A + B@i
5. case a1 of inl(a) => inr a  | inr(b) => inl b = case a2 of inl(a) => inr a  | inr(b) => inl b ∈ (B + A)
⊢ a1 = a2 ∈ (A + B)

2
1. [A] : Type
2. [B] : Type
3. b : B + A@i
⊢ ∃a:A + B. (case a of inl(a) => inr a  | inr(b) => inl b = b ∈ (B + A))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    A  +  B  \msim{}  B  +  A


By

---

Latex:
TACTIC:((Auto  THEN  With  \mkleeneopen{}\mlambda{}x.case  x  of  inl(a)  =>  inr  a    |  inr(b)  =>  inl  b\mkleeneclose{}  (D  0)\mcdot{})
                THEN  Auto
                THEN  RepeatFor  2  (D  0)
                THEN  Reduce  0
                THEN  Auto)

---

Home Index