---

Step * of Lemma union_functionality_wrt_equipollent

∀[A,B,C,D:Type].  (A ~ B ⇒ C ~ D ⇒ A + C ~ B + D)
BY
{ TACTIC:(Auto THEN D -2 THEN D -1 THEN RenameVar `g' (-2)) }

1
1. [A] : Type
2. [B] : Type
3. [C] : Type
4. [D] : Type
5. f : A ⟶ B@i
6. Bij(A;B;f)
7. g : C ⟶ D@i
8. Bij(C;D;g)
⊢ A + C ~ B + D

---

Latex:

---

Latex:
\mforall{}[A,B,C,D:Type].    (A  \msim{}  B  {}\mRightarrow{}  C  \msim{}  D  {}\mRightarrow{}  A  +  C  \msim{}  B  +  D)


By

---

Latex:
TACTIC:(Auto  THEN  D  -2  THEN  D  -1  THEN  RenameVar  `g'  (-2))

---

Home Index