---

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


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)
BY
{ (ParallelOp 2 THEN MoveToConcl (-1) THEN GenConclAtAddr [1;1] THEN D -2 THEN Reduce 0 THEN Auto) }

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))
4. i : ℕ||L||
5. X : Type
6. v1 : X ⟶ X ⟶ ℙ
7. L[i] = <X, v1> ∈ (X:Type × (X ⟶ X ⟶ ℙ))
8. EquivRel(X;x,y.v1 x y)
⊢ v1 a.i a.i

---

Latex:

---

Latex:

1.  L  :  (X:Type  \mtimes{}  (X  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}))  List
2.  \mforall{}i:\mBbbN{}||L||.  let  X,E  =  L[i]  in  EquivRel(X;x,y.E  x  y)
3.  a  :  tuple-type(map(\mlambda{}p.(fst(p));L))
\mvdash{}  \mforall{}i:\mBbbN{}||L||.  ((snd(L[i]))  a.i  a.i)


By

---

Latex:
(ParallelOp  2  THEN  MoveToConcl  (-1)  THEN  GenConclAtAddr  [1;1]  THEN  D  -2  THEN  Reduce  0  THEN  Auto)

---

Home Index