---

Step * of Lemma simple-comb1_wf

∀[Info,A,B:Type]. ∀[F:bag(A) ⟶ bag(B)]. ∀[X:EClass(A)].  (λx.F[x]|X| ∈ EClass(B))
BY
{ ProveWfLemma⋅ }

1
1. Info : Type
2. A : Type
3. B : Type
4. F : bag(A) ⟶ bag(B)
5. X : EClass(A)
⊢ simple-comb(λw.F[w 0];λz.[X][z]) ∈ EClass(B)

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[F:bag(A)  {}\mrightarrow{}  bag(B)].  \mforall{}[X:EClass(A)].    (\mlambda{}x.F[x]|X|  \mmember{}  EClass(B))


By

---

Latex:
ProveWfLemma\mcdot{}

---

Home Index