---

Step * of Lemma lifting1-loc_wf

∀[A,B:Type]. ∀[f:Id ⟶ A ⟶ B]. ∀[loc:Id]. ∀[b:bag(A)].  (lifting1-loc(f;loc;b) ∈ bag(B))
BY
{ (ProveWfLemma
   THEN InstLemma `lifting-loc-gen-rev_wf` [⌜B⌝; ⌜1⌝; ⌜λx.A⌝; ⌜λx.b⌝; ⌜loc⌝; ⌜f⌝]⋅
   THEN Try (Reduce 0)
   THEN Auto
   THEN Unfold `funtype` 0
   THEN Repeat (((RWO "primrec-unroll" 0 THENM Reduce 0) THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B].  \mforall{}[loc:Id].  \mforall{}[b:bag(A)].    (lifting1-loc(f;loc;b)  \mmember{}  bag(B))


By

---

Latex:
(ProveWfLemma
  THEN  InstLemma  `lifting-loc-gen-rev\_wf`  [\mkleeneopen{}B\mkleeneclose{};  \mkleeneopen{}1\mkleeneclose{};  \mkleeneopen{}\mlambda{}x.A\mkleeneclose{};  \mkleeneopen{}\mlambda{}x.b\mkleeneclose{};  \mkleeneopen{}loc\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{}]\mcdot{}
  THEN  Try  (Reduce  0)
  THEN  Auto
  THEN  Unfold  `funtype`  0
  THEN  Repeat  (((RWO  "primrec-unroll"  0  THENM  Reduce  0)  THEN  Auto)))

---

Home Index