Step
*
of Lemma
for_hdtl_wf
∀[A,B,C:Type]. ∀[f:B ⟶ C ⟶ C]. ∀[k:C]. ∀[as:A List]. ∀[g:A ⟶ (A List) ⟶ B]. (ForHdTl{A,f,k} h::t ∈ as. g[h;t] ∈ C)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[A,B,C:Type]. \mforall{}[f:B {}\mrightarrow{} C {}\mrightarrow{} C]. \mforall{}[k:C]. \mforall{}[as:A List]. \mforall{}[g:A {}\mrightarrow{} (A List) {}\mrightarrow{} B].
(ForHdTl\{A,f,k\} h::t \mmember{} as. g[h;t] \mmember{} C)
By
Latex:
ProveWfLemma
Home
Index