---

Step * 1 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))
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
BY
{ ((Assert a.i ∈ X BY
          (DoSubsume THEN Auto THEN RWO "select-map" 0 THEN Reduce 0 THEN Auto THEN RWO "-3" 0 THEN Auto))
   THEN Auto
   ) }

---

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))
4.  i  :  \mBbbN{}||L||
5.  X  :  Type
6.  v1  :  X  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}
7.  L[i]  =  <X,  v1>
8.  EquivRel(X;x,y.v1  x  y)
\mvdash{}  v1  a.i  a.i


By

---

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

---

Home Index