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