---

Step * 1 1 1 1 of Lemma local-class-equality


1. Info : Type
2. x : Id
3. inputs : Info List
4. a : Info
5. es : EO+(Info)
6. e : E
7. loc(e) = x ∈ Id
8. (inputs @ [a]) = map(λe.info(e);≤loc(e)) ∈ (Info List)
⊢ (loc(e) = x ∈ Id) ∧ (map(λx.info(x);before(e)) = inputs ∈ (Info List)) ∧ (info(e) = a ∈ Info)
BY
{ Unfold `es-le-before` (-1) }

1
1. Info : Type
2. x : Id
3. inputs : Info List
4. a : Info
5. es : EO+(Info)
6. e : E
7. loc(e) = x ∈ Id
8. (inputs @ [a]) = map(λe.info(e);before(e) @ [e]) ∈ (Info List)
⊢ (loc(e) = x ∈ Id) ∧ (map(λx.info(x);before(e)) = inputs ∈ (Info List)) ∧ (info(e) = a ∈ Info)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  x  :  Id
3.  inputs  :  Info  List
4.  a  :  Info
5.  es  :  EO+(Info)
6.  e  :  E
7.  loc(e)  =  x
8.  (inputs  @  [a])  =  map(\mlambda{}e.info(e);\mleq{}loc(e))
\mvdash{}  (loc(e)  =  x)  \mwedge{}  (map(\mlambda{}x.info(x);before(e))  =  inputs)  \mwedge{}  (info(e)  =  a)


By

---

Latex:
Unfold  `es-le-before`  (-1)

---

Home Index