---

Step * 1 of Lemma lifting-loc-3_wf

.....wf..... 
1. A : Type
2. B : Type
3. C : Type
4. D : Type
5. f : Id ─→ A ─→ B ─→ C ─→ D
6. l : Id@i
7. a : bag(A)@i
8. b : bag(B)@i
9. c : bag(C)@i
⊢ f ∈ Id ─→ funtype(3;λn.[A; B; C][n];D)
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.  D  :  Type
5.  f  :  Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C  {}\mrightarrow{}  D
6.  l  :  Id@i
7.  a  :  bag(A)@i
8.  b  :  bag(B)@i
9.  c  :  bag(C)@i
\mvdash{}  f  \mmember{}  Id  {}\mrightarrow{}  funtype(3;\mlambda{}n.[A;  B;  C][n];D)


By

---

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

---

Home Index