---

Step * 3 1 of Lemma tuple-equiv-is-equiv


1. L : (X:Type × (X ⟶ X ⟶ ℙ)) List
2. Sym(tuple-type(map(λp.(fst(p));L));t,t'.∀i:ℕ||L||. ((snd(L[i])) t.i t'.i))
3. a : tuple-type(map(λp.(fst(p));L))
4. b : tuple-type(map(λp.(fst(p));L))
5. c : tuple-type(map(λp.(fst(p));L))
6. ∀i:ℕ||L||. ((snd(L[i])) b.i c.i)
7. i : ℕ||L||
8. X : Type
9. v1 : X ⟶ X ⟶ ℙ
10. L[i] = <X, v1> ∈ (X:Type × (X ⟶ X ⟶ ℙ))
⊢ EquivRel(X;x,y.v1 x y) ⇒ (v1 a.i b.i) ⇒ (v1 b.i c.i) ⇒ (v1 a.i c.i)
BY
{ (Assert a.i ∈ X BY
         (DoSubsume THEN Auto THEN RWO "select-map" 0 THEN Reduce 0 THEN Auto THEN RWO "-2" 0 THEN Auto)) }

1
1. L : (X:Type × (X ⟶ X ⟶ ℙ)) List
2. Sym(tuple-type(map(λp.(fst(p));L));t,t'.∀i:ℕ||L||. ((snd(L[i])) t.i t'.i))
3. a : tuple-type(map(λp.(fst(p));L))
4. b : tuple-type(map(λp.(fst(p));L))
5. c : tuple-type(map(λp.(fst(p));L))
6. ∀i:ℕ||L||. ((snd(L[i])) b.i c.i)
7. i : ℕ||L||
8. X : Type
9. v1 : X ⟶ X ⟶ ℙ
10. L[i] = <X, v1> ∈ (X:Type × (X ⟶ X ⟶ ℙ))
11. a.i ∈ X
⊢ EquivRel(X;x,y.v1 x y) ⇒ (v1 a.i b.i) ⇒ (v1 b.i c.i) ⇒ (v1 a.i c.i)

---

Latex:

---

Latex:

1.  L  :  (X:Type  \mtimes{}  (X  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}))  List
2.  Sym(tuple-type(map(\mlambda{}p.(fst(p));L));t,t'.\mforall{}i:\mBbbN{}||L||.  ((snd(L[i]))  t.i  t'.i))
3.  a  :  tuple-type(map(\mlambda{}p.(fst(p));L))
4.  b  :  tuple-type(map(\mlambda{}p.(fst(p));L))
5.  c  :  tuple-type(map(\mlambda{}p.(fst(p));L))
6.  \mforall{}i:\mBbbN{}||L||.  ((snd(L[i]))  b.i  c.i)
7.  i  :  \mBbbN{}||L||
8.  X  :  Type
9.  v1  :  X  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}
10.  L[i]  =  <X,  v1>
\mvdash{}  EquivRel(X;x,y.v1  x  y)  {}\mRightarrow{}  (v1  a.i  b.i)  {}\mRightarrow{}  (v1  b.i  c.i)  {}\mRightarrow{}  (v1  a.i  c.i)


By

---

Latex:
(Assert  a.i  \mmember{}  X  BY
              (DoSubsume
                THEN  Auto
                THEN  RWO  "select-map"  0
                THEN  Reduce  0
                THEN  Auto
                THEN  RWO  "-2"  0
                THEN  Auto))

---

Home Index