---

Step * of Lemma lifting2_wf

∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[abag:bag(A)]. ∀[bbag:bag(B)].  (lifting2(f;abag;bbag) ∈ bag(C))
BY
{ (ProveWfLemma
   THEN InstLemma `lifting-gen-rev_wf` [⌜C⌝; ⌜2⌝; ⌜λx.[A; B][x]⌝; ⌜λx.[abag; bbag][x]⌝; ⌜f⌝]⋅
   THEN Try (Complete (Auto))) }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  C].  \mforall{}[abag:bag(A)].  \mforall{}[bbag:bag(B)].    (lifting2(f;abag;bbag)  \mmember{}  bag(C))


By

---

Latex:
(ProveWfLemma
  THEN  InstLemma  `lifting-gen-rev\_wf`  [\mkleeneopen{}C\mkleeneclose{};  \mkleeneopen{}2\mkleeneclose{};  \mkleeneopen{}\mlambda{}x.[A;  B][x]\mkleeneclose{};  \mkleeneopen{}\mlambda{}x.[abag;  bbag][x]\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{}]\mcdot{}
  THEN  Try  (Complete  (Auto)))

---

Home Index