Step
*
1
of Lemma
map2_wf
.....aux.....
1. T : Type
2. value-type(T)
3. A : Type
4. B : Type
5. f : A ⟶ B ⟶ T
6. u : A
7. v : A List
8. ∀[bs:B List]. (map2(f;v;bs) ∈ T List)
9. u1 : B
10. v1 : B List
11. map2(f;[u / v];v1) ∈ T List
⊢ (map2(f;v;v1))↓
BY
{ (InstHyp [⌜v1⌝] (-4)⋅ THEN Auto) }
Latex:
Latex:
.....aux.....
1. T : Type
2. value-type(T)
3. A : Type
4. B : Type
5. f : A {}\mrightarrow{} B {}\mrightarrow{} T
6. u : A
7. v : A List
8. \mforall{}[bs:B List]. (map2(f;v;bs) \mmember{} T List)
9. u1 : B
10. v1 : B List
11. map2(f;[u / v];v1) \mmember{} T List
\mvdash{} (map2(f;v;v1))\mdownarrow{}
By
Latex:
(InstHyp [\mkleeneopen{}v1\mkleeneclose{}] (-4)\mcdot{} THEN Auto)
Home
Index