---

Step * 1 1 of Lemma global-eo-info-before


1. L : (Id × Top) List
2. e : {e:ℕ||L||| True} 
3. v : ℕe List@i
4. upto(e) = v ∈ (ℕe List)@i
⊢ map(λe.(snd(L[e]));filter(λn.fst(L[n]) = fst(L[e]);v)) ~ map(λx.(snd(x));filter(λx.fst(x) = fst(L[e]);map(λi.L[i];v)))
BY
{ (Thin (-1) THEN ListInd (-1) THEN Reduce 0 THEN Try (AutoSplit)) }

1
1. L : (Id × Top) List
2. e : {e:ℕ||L||| True} 
⊢ [] ~ []

---

Latex:

---

Latex:

1.  L  :  (Id  \mtimes{}  Top)  List
2.  e  :  \{e:\mBbbN{}||L|||  True\} 
3.  v  :  \mBbbN{}e  List@i
4.  upto(e)  =  v@i
\mvdash{}  map(\mlambda{}e.(snd(L[e]));filter(\mlambda{}n.fst(L[n])  =  fst(L[e]);v)) 
\msim{}  map(\mlambda{}x.(snd(x));filter(\mlambda{}x.fst(x)  =  fst(L[e]);map(\mlambda{}i.L[i];v)))


By

---

Latex:
(Thin  (-1)  THEN  ListInd  (-1)  THEN  Reduce  0  THEN  Try  (AutoSplit))

---

Home Index