---

Step * 1 of Lemma lifting2-loc_wf

.....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)
BY
{ (Unfold `funtype` 0 THEN Repeat (((RWO "primrec-unroll" 0 THENM Reduce 0) THEN Auto))) }

---

Latex:

---

Latex:
.....wf..... 
1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  f  :  Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C
5.  loc  :  Id
6.  abag  :  bag(A)
7.  bbag  :  bag(B)
\mvdash{}  f  \mmember{}  Id  {}\mrightarrow{}  funtype(2;\mlambda{}x.[A;  B][x];C)


By

---

Latex:
(Unfold  `funtype`  0  THEN  Repeat  (((RWO  "primrec-unroll"  0  THENM  Reduce  0)  THEN  Auto)))

---

Home Index