---

Step * 1 of Lemma es-interface-restrict-conditional


1. Info : Type
2. A : Type
3. I : EClass(A)
4. P : es:EO+(Info) ⟶ E ⟶ ℙ
5. p : ∀es:EO+(Info). ∀e:E.  Dec(P[es;e])
6. Singlevalued(I)
7. x : EO+(Info)
8. x1 : E
9. x2 : P[x;x1]@i
10. (p x x1) = (inl x2) ∈ Dec(P[x;x1])@i
⊢ if (#(I x x1) =z 1) then I x x1 else {} fi  = (I x x1) ∈ bag(A)
BY
{ (Symmetry THEN BLemma `sv-class-iff` THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  I  :  EClass(A)
4.  P  :  es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
5.  p  :  \mforall{}es:EO+(Info).  \mforall{}e:E.    Dec(P[es;e])
6.  Singlevalued(I)
7.  x  :  EO+(Info)
8.  x1  :  E
9.  x2  :  P[x;x1]@i
10.  (p  x  x1)  =  (inl  x2)@i
\mvdash{}  if  (\#(I  x  x1)  =\msubz{}  1)  then  I  x  x1  else  \{\}  fi    =  (I  x  x1)


By

---

Latex:
(Symmetry  THEN  BLemma  `sv-class-iff`  THEN  Auto)

---

Home Index