---

Step * of Lemma simple-loc-comb-0_wf

∀[Info,B:Type]. ∀[b:Id ⟶ bag(B)].  (simple-loc-comb-0(b) ∈ EClass(B))
BY
{ (ProveWfLemma THEN InstLemma `simple-loc-comb_wf` [⌜Info⌝; ⌜B⌝; ⌜0⌝; ⌜λn.[][n]⌝; ⌜λn.[][n]⌝; ⌜λl,w. (b l)⌝]⋅ THEN Auto\000C) }

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].  \mforall{}[b:Id  {}\mrightarrow{}  bag(B)].    (simple-loc-comb-0(b)  \mmember{}  EClass(B))


By

---

Latex:
(ProveWfLemma
  THEN  InstLemma  `simple-loc-comb\_wf`  [\mkleeneopen{}Info\mkleeneclose{};  \mkleeneopen{}B\mkleeneclose{};  \mkleeneopen{}0\mkleeneclose{};  \mkleeneopen{}\mlambda{}n.[][n]\mkleeneclose{};  \mkleeneopen{}\mlambda{}n.[][n]\mkleeneclose{};  \mkleeneopen{}\mlambda{}l,w.  (b  l)\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index