---

Step * 1 1 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);before(e)) @ [info(e)]) ∈ (Info List)
⊢ (loc(e) = x ∈ Id) ∧ (map(λx.info(x);before(e)) = inputs ∈ (Info List)) ∧ (info(e) = a ∈ Info)
BY
{ AutoSimpHyp Auto (-1) }

---

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);before(e))  @  [info(e)])
\mvdash{}  (loc(e)  =  x)  \mwedge{}  (map(\mlambda{}x.info(x);before(e))  =  inputs)  \mwedge{}  (info(e)  =  a)


By

---

Latex:
AutoSimpHyp  Auto  (-1)

---

Home Index