---

Step * of Lemma respects-equality-product

∀[A,A':Type]. ∀[B:A ⟶ Type]. ∀[B':A' ⟶ Type].
  (respects-equality(A;A')
  ⇒ (∀a:Base. ((a ∈ A) ⇒ (a ∈ A') ⇒ respects-equality(B[a];B'[a])))
  ⇒ respects-equality(a:A × B[a];a:A' × B'[a]))
BY
{ (Auto
   THEN RepeatFor 4 ((D 0 THENW Auto))
   THEN (Assert x ~ <fst(x), snd(x)> BY
               ((GenConclTerm ⌜x⌝⋅ THEN Auto) THEN (D -2 THEN Reduce 0) THEN Auto))
   THEN (Assert y ~ <fst(y), snd(y)> BY
               ((GenConcl ⌜y = v ∈ (a:A × B[a])⌝⋅ THENA Auto) THEN (D -2 THEN Reduce 0) THEN Auto))
   THEN (Assert <fst(x), snd(x)> = <fst(y), snd(y)> ∈ (a:A × B[a]) BY
               (NthHypSq (-4) THEN SqEqCD THEN Auto))
   THEN (Assert ⌜<fst(x), snd(x)> = <fst(y), snd(y)> ∈ (a:A' × B'[a])⌝⋅ THENM (NthHypSq (-1) THEN SqEqCD THEN Auto))
   THEN (EqHD (-1) THENA Auto)
   THEN (EqCD THENA Auto)
   THEN All Reduce) }

1
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)]
⊢ (fst(x)) = (fst(y)) ∈ A'

2
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)]

---

Latex:

---

Latex:
\mforall{}[A,A':Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[B':A'  {}\mrightarrow{}  Type].
    (respects-equality(A;A')
    {}\mRightarrow{}  (\mforall{}a:Base.  ((a  \mmember{}  A)  {}\mRightarrow{}  (a  \mmember{}  A')  {}\mRightarrow{}  respects-equality(B[a];B'[a])))
    {}\mRightarrow{}  respects-equality(a:A  \mtimes{}  B[a];a:A'  \mtimes{}  B'[a]))


By

---

Latex:
(Auto
  THEN  RepeatFor  4  ((D  0  THENW  Auto))
  THEN  (Assert  x  \msim{}  <fst(x),  snd(x)>  BY
                          ((GenConclTerm  \mkleeneopen{}x\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  (D  -2  THEN  Reduce  0)  THEN  Auto))
  THEN  (Assert  y  \msim{}  <fst(y),  snd(y)>  BY
                          ((GenConcl  \mkleeneopen{}y  =  v\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (D  -2  THEN  Reduce  0)  THEN  Auto))
  THEN  (Assert  <fst(x),  snd(x)>  =  <fst(y),  snd(y)>  BY
                          (NthHypSq  (-4)  THEN  SqEqCD  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}<fst(x),  snd(x)>  =  <fst(y),  snd(y)>\mkleeneclose{}\mcdot{}  THENM  (NthHypSq  (-1)  THEN  SqEqCD  THEN  Auto))
  THEN  (EqHD  (-1)  THENA  Auto)
  THEN  (EqCD  THENA  Auto)
  THEN  All  Reduce)

---

Home Index