---

Step * 1 of Lemma equipollent-union-function


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)
BY
{ TACTIC:(SplitPair (-1) THEN (Ext THEN Auto) THEN D -1) }

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))) = (λa.(a2 (inl a))) ∈ (A ⟶ C)
7. (λb.(a1 (inr b ))) = (λb.(a2 (inr b ))) ∈ (B ⟶ C)
8. x1 : A
⊢ (a1 (inl x1)) = (a2 (inl x1)) ∈ C

2
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))) = (λa.(a2 (inl a))) ∈ (A ⟶ C)
7. (λb.(a1 (inr b ))) = (λb.(a2 (inr b ))) ∈ (B ⟶ C)
8. y : B
⊢ (a1 (inr y )) = (a2 (inr y )) ∈ C

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  a1  :  (A  +  B)  {}\mrightarrow{}  C@i
5.  a2  :  (A  +  B)  {}\mrightarrow{}  C@i
6.  <\mlambda{}a.(a1  (inl  a)),  \mlambda{}b.(a1  (inr  b  ))>  =  <\mlambda{}a.(a2  (inl  a)),  \mlambda{}b.(a2  (inr  b  ))>
\mvdash{}  a1  =  a2


By

---

Latex:
TACTIC:(SplitPair  (-1)  THEN  (Ext  THEN  Auto)  THEN  D  -1)

---

Home Index