---

Step * 2 of Lemma respects-equality-union


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
BY
{ ((D 6 With ⌜outr(x)⌝  THENA Auto) THEN BHyp -1 THEN Auto THEN HypSubst' (-5) 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

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)  )
10.  x  \mmember{}  T1  +  T2
11.  x  \msim{}  inr  outr(x) 
12.  y  \msim{}  inr  outr(y) 
13.  (inr  outr(x)  )  =  (inr  outr(y)  )
14.  outr(x)  =  outr(y)
\mvdash{}  outr(x)  =  outr(y)


By

---

Latex:
((D  6  With  \mkleeneopen{}outr(x)\mkleeneclose{}    THENA  Auto)
  THEN  BHyp  -1
  THEN  Auto
  THEN  HypSubst'  (-5)  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index