---

Step * of Lemma cond-class-val

∀[Info,A:Type]. ∀[X,Y:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
  [X?Y](e) = if e ∈b X then X(e) else Y(e) fi  ∈ A supposing ↑e ∈b [X?Y]
BY
{ (RepeatFor 6 ((D 0 THENA Auto)) THEN (RepUR ``in-eclass cond-class eclass-compose2 eclass-val`` 0⋅ THEN AutoSplit)) }

1
1. Info : Type
2. A : Type
3. X : EClass(A)
4. Y : EClass(A)
5. es : EO+(Info)
6. e : E
7. #(X es e) = 1 ∈ ℤ
⊢ only(X es e) = only(X es e) ∈ A supposing ↑(#(X es e) =z 1)

2
1. Info : Type
2. A : Type
3. X : EClass(A)
4. Y : EClass(A)
5. es : EO+(Info)
6. e : E
7. #(X es e) ≠ 1
⊢ only(Y es e) = only(Y es e) ∈ A supposing ↑(#(Y es e) =z 1)

---

Latex:


\mforall{}[Info,A:Type].  \mforall{}[X,Y:EClass(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    [X?Y](e)  =  if  e  \mmember{}\msubb{}  X  then  X(e)  else  Y(e)  fi    supposing  \muparrow{}e  \mmember{}\msubb{}  [X?Y]


By

(RepeatFor  6  ((D  0  THENA  Auto))
  THEN  (RepUR  ``in-eclass  cond-class  eclass-compose2  eclass-val``  0\mcdot{}  THEN  AutoSplit)
  )

---

Home Index