---

Step * of Lemma simple-loc-comb-1-concat-classrel

∀[Info,A,B:Type]. ∀[f:Id ⟶ A ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
  uiff(v ∈ f@(Loc, X)(e);↓∃a:A. (a ∈ X(e) ∧ v ↓∈ f loc(e) a))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``concat-lifting-loc-1 simple-loc-comb-1`` 0
   THEN (InstLemma `simple-loc-comb1-concat-classrel` [⌜Info⌝;⌜A⌝;⌜B⌝;⌜f⌝;⌜X⌝;⌜es⌝;⌜e⌝;⌜v⌝]⋅ THENA Auto)
   THEN Unfold `simple-loc-comb1` (-1)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  bag(B)].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:B].
    uiff(v  \mmember{}  f@(Loc,  X)(e);\mdownarrow{}\mexists{}a:A.  (a  \mmember{}  X(e)  \mwedge{}  v  \mdownarrow{}\mmember{}  f  loc(e)  a))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``concat-lifting-loc-1  simple-loc-comb-1``  0
  THEN  (InstLemma  `simple-loc-comb1-concat-classrel`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Unfold  `simple-loc-comb1`  (-1)
  THEN  Trivial)

---

Home Index