---

Step * of Lemma lifting2-loc_wf

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

1
.....wf..... 
1. A : Type
2. B : Type
3. C : Type
4. f : Id ⟶ A ⟶ B ⟶ C
5. loc : Id
6. abag : bag(A)
7. bbag : bag(B)
⊢ f ∈ Id ⟶ funtype(2;λx.[A; B][x];C)

---

Latex:

---

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


By

---

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

---

Home Index