---

Step * of Lemma respects-equality-union

∀[T1,T2,S1,S2:Type].  (respects-equality(S1;T1) ⇒ respects-equality(S2;T2) ⇒ respects-equality(S1 + S2;T1 + T2))
BY
{ (Intros
   THEN RepeatFor 4 ((D 0 THENA Auto))
   THEN (InstLemma `union-eta` [⌜x⌝]⋅ THENA Auto)
   THEN D -1
   THEN HypSubst' (-1) 0
   THEN HypSubst' (-1) (-3)
   THEN (InstLemma `union-eta` [⌜y⌝]⋅ THENA Auto)
   THEN D -1
   THEN HypSubst' (-1) 0
   THEN HypSubst' (-1) (-4)
   THEN (EqCDA ORELSE Auto)
   THEN StrengthenEquation (-4)
   THEN ((ApFunToHypEquands `Z' ⌜outr(Z)⌝ ⌜S2⌝ (-1)⋅ THENA Complete (Auto))
   ORELSE (ApFunToHypEquands `Z' ⌜outl(Z)⌝ ⌜S1⌝ (-1)⋅ THENA Complete (Auto))
   )
   THEN Reduce -1) }

1
1. T1 : Type
2. T2 : Type
3. S1 : Type
4. S2 : Type
5. respects-equality(S1;T1)
6. respects-equality(S2;T2)
7. x : Base
8. y : Base
9. (inl outl(x)) = (inl outl(y)) ∈ (S1 + S2)
10. x ∈ T1 + T2
11. x ~ inl outl(x)
12. y ~ inl outl(y)
13. (inl outl(x)) = (inl outl(y)) ∈ {z:S1 + S2| (z = (inl outl(x)) ∈ (S1 + S2)) ∧ (z = (inl outl(y)) ∈ (S1 + S2))} 
14. outl(x) = outl(y) ∈ S1
⊢ outl(x) = outl(y) ∈ T1

2
1. T1 : Type
2. T2 : Type
3. S1 : Type
4. S2 : Type
5. respects-equality(S1;T1)
6. respects-equality(S2;T2)
7. x : Base
8. y : Base
9. (inr outr(x) ) = (inr outr(y) ) ∈ (S1 + S2)
10. x ∈ T1 + T2
11. x ~ inr outr(x) 
12. y ~ inr outr(y) 
13. (inr outr(x) ) = (inr outr(y) ) ∈ {z:S1 + S2| (z = (inr outr(x) ) ∈ (S1 + S2)) ∧ (z = (inr outr(y) ) ∈ (S1 + S2))} 
14. outr(x) = outr(y) ∈ S2
⊢ outr(x) = outr(y) ∈ T2

---

Latex:

---

Latex:
\mforall{}[T1,T2,S1,S2:Type].
    (respects-equality(S1;T1)  {}\mRightarrow{}  respects-equality(S2;T2)  {}\mRightarrow{}  respects-equality(S1  +  S2;T1  +  T2))


By

---

Latex:
(Intros
  THEN  RepeatFor  4  ((D  0  THENA  Auto))
  THEN  (InstLemma  `union-eta`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  HypSubst'  (-1)  0
  THEN  HypSubst'  (-1)  (-3)
  THEN  (InstLemma  `union-eta`  [\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  HypSubst'  (-1)  0
  THEN  HypSubst'  (-1)  (-4)
  THEN  (EqCDA  ORELSE  Auto)
  THEN  StrengthenEquation  (-4)
  THEN  ((ApFunToHypEquands  `Z'  \mkleeneopen{}outr(Z)\mkleeneclose{}  \mkleeneopen{}S2\mkleeneclose{}  (-1)\mcdot{}  THENA  Complete  (Auto))
  ORELSE  (ApFunToHypEquands  `Z'  \mkleeneopen{}outl(Z)\mkleeneclose{}  \mkleeneopen{}S1\mkleeneclose{}  (-1)\mcdot{}  THENA  Complete  (Auto))
  )
  THEN  Reduce  -1)

---

Home Index