---

Step * of Lemma equipollent-union-function

∀[A,B,C:Type].  (A + B) ⟶ C ~ A ⟶ C × (B ⟶ C)
BY
{ TACTIC:(Auto
          THEN TACTIC:(Auto
                       THEN With ⌜λf.<λa.(f (inl a)), λb.(f (inr b ))>⌝ (D 0)⋅
                       THEN Auto
                       THEN RepeatFor 2 ((D 0 THEN Reduce 0 THEN Auto)))
          ) }

1
1. A : Type
2. B : Type
3. C : Type
4. a1 : (A + B) ⟶ C@i
5. a2 : (A + B) ⟶ C@i
6. <λa.(a1 (inl a)), λb.(a1 (inr b ))> = <λa.(a2 (inl a)), λb.(a2 (inr b ))> ∈ (A ⟶ C × (B ⟶ C))
⊢ a1 = a2 ∈ ((A + B) ⟶ C)

2
1. [A] : Type
2. [B] : Type
3. [C] : Type
4. b : A ⟶ C × (B ⟶ C)@i
⊢ ∃a:(A + B) ⟶ C. (<λa@0.(a (inl a@0)), λb.(a (inr b ))> = b ∈ (A ⟶ C × (B ⟶ C)))

---

Latex:

---

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


By

---

Latex:
TACTIC:(Auto
                THEN  TACTIC:(Auto
                                          THEN  With  \mkleeneopen{}\mlambda{}f.<\mlambda{}a.(f  (inl  a)),  \mlambda{}b.(f  (inr  b  ))>\mkleeneclose{}  (D  0)\mcdot{}
                                          THEN  Auto
                                          THEN  RepeatFor  2  ((D  0  THEN  Reduce  0  THEN  Auto)))
                )

---

Home Index