---

Step * 2 of Lemma respects-equality-product


1. A : Type
2. A' : Type
3. B : A ⟶ Type
4. B' : A' ⟶ Type
5. respects-equality(A;A')
6. ∀a:Base. ((a ∈ A) ⇒ (a ∈ A') ⇒ respects-equality(B[a];B'[a]))
7. x : Base
8. y : Base
9. x = y ∈ (a:A × B[a])
10. x ∈ a:A' × B'[a]
11. x ~ <fst(x), snd(x)>
12. y ~ <fst(y), snd(y)>
13. (fst(x)) = (fst(y)) ∈ A
14. (snd(x)) = (snd(y)) ∈ B[fst(x)]
⊢ (snd(x)) = (snd(y)) ∈ B'[fst(x)]
BY
{ (BackThruHyp' 6 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  A'  :  Type
3.  B  :  A  {}\mrightarrow{}  Type
4.  B'  :  A'  {}\mrightarrow{}  Type
5.  respects-equality(A;A')
6.  \mforall{}a:Base.  ((a  \mmember{}  A)  {}\mRightarrow{}  (a  \mmember{}  A')  {}\mRightarrow{}  respects-equality(B[a];B'[a]))
7.  x  :  Base
8.  y  :  Base
9.  x  =  y
10.  x  \mmember{}  a:A'  \mtimes{}  B'[a]
11.  x  \msim{}  <fst(x),  snd(x)>
12.  y  \msim{}  <fst(y),  snd(y)>
13.  (fst(x))  =  (fst(y))
14.  (snd(x))  =  (snd(y))
\mvdash{}  (snd(x))  =  (snd(y))


By

---

Latex:
(BackThruHyp'  6  THEN  Auto)

---

Home Index