---

Step * of Lemma tuple-equiv-is-equiv

∀L:(X:Type × (X ⟶ X ⟶ ℙ)) List
  ((∀i:ℕ||L||. let X,E = L[i] in EquivRel(X;x,y.E x y))
  ⇒ EquivRel(tuple-type(map(λp.(fst(p));L));t,t'.tuple-equiv(L) t t'))
BY
{ (Auto THEN D 0 THEN Auto THEN D 0 THEN Auto THEN All (RepUR ``tuple-equiv let``)) }

1
1. L : (X:Type × (X ⟶ X ⟶ ℙ)) List
2. ∀i:ℕ||L||. let X,E = L[i] in EquivRel(X;x,y.E x y)
3. a : tuple-type(map(λp.(fst(p));L))
⊢ ∀i:ℕ||L||. ((snd(L[i])) a.i a.i)

2
1. L : (X:Type × (X ⟶ X ⟶ ℙ)) List
2. ∀i:ℕ||L||. let X,E = L[i] in EquivRel(X;x,y.E x y)
3. a : tuple-type(map(λp.(fst(p));L))
4. b : tuple-type(map(λp.(fst(p));L))
5. ∀i:ℕ||L||. ((snd(L[i])) a.i b.i)
⊢ ∀i:ℕ||L||. ((snd(L[i])) b.i a.i)

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

---

Latex:

---

Latex:
\mforall{}L:(X:Type  \mtimes{}  (X  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}))  List
    ((\mforall{}i:\mBbbN{}||L||.  let  X,E  =  L[i]  in  EquivRel(X;x,y.E  x  y))
    {}\mRightarrow{}  EquivRel(tuple-type(map(\mlambda{}p.(fst(p));L));t,t'.tuple-equiv(L)  t  t'))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  D  0  THEN  Auto  THEN  All  (RepUR  ``tuple-equiv  let``))

---

Home Index