---

Step * 1 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. (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
BY
{ ((D 5 With ⌜outl(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.  (inl  outl(x))  =  (inl  outl(y))
10.  x  \mmember{}  T1  +  T2
11.  x  \msim{}  inl  outl(x)
12.  y  \msim{}  inl  outl(y)
13.  (inl  outl(x))  =  (inl  outl(y))
14.  outl(x)  =  outl(y)
\mvdash{}  outl(x)  =  outl(y)


By

---

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

---

Home Index