---

Step * 1 of Lemma simple-comb1_wf


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)
BY
{ ((InstLemma `simple-comb_wf` [⌈Info⌉;⌈B⌉;⌈1⌉;⌈λ2x.A⌉]⋅ THENA Auto) THEN BHyp -1  THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  F  :  bag(A)  {}\mrightarrow{}  bag(B)
5.  X  :  EClass(A)
\mvdash{}  simple-comb(\mlambda{}w.F[w  0];\mlambda{}z.[X][z])  \mmember{}  EClass(B)


By

---

Latex:
((InstLemma  `simple-comb\_wf`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.A\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  BHyp  -1    THEN  Auto')\mcdot{}

---

Home Index