---

Step * of Lemma parallel-as-bind

∀[A,Info:Type]. ∀[X,Y:EClass(A)].  (X || Y = return-bag-class(tt.ff.{}) >b> if b then X else Y fi  ∈ EClass(A))
BY
{ (UnivCD THENA Auto) }

1
1. A : Type
2. Info : Type
3. X : EClass(A)
4. Y : EClass(A)
⊢ X || Y = return-bag-class(tt.ff.{}) >b> if b then X else Y fi  ∈ EClass(A)

---

Latex:

---

Latex:
\mforall{}[A,Info:Type].  \mforall{}[X,Y:EClass(A)].    (X  ||  Y  =  return-bag-class(tt.ff.\{\})  >b>  if  b  then  X  else  Y  fi  )


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index