Step
*
of Lemma
A-bind2_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[T,S:Type]. ∀[m:A-map T]. ∀[k:T ⟶ (A-map S)].
(m >> \x.
k[x] ∈ A-map S)
BY
{ (ProveWfLemma THEN InstLemma `A-bind_wf` [⌜Val⌝;⌜n⌝;⌜AType⌝;⌜T⌝;⌜S⌝]⋅ THEN Auto) }
Latex:
Latex:
\mforall{}[Val:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[AType:array\{i:l\}(Val;n)]. \mforall{}[T,S:Type]. \mforall{}[m:A-map T]. \mforall{}[k:T {}\mrightarrow{} (A-map S)].
(m >> \mbackslash{}x.
k[x] \mmember{} A-map S)
By
Latex:
(ProveWfLemma THEN InstLemma `A-bind\_wf` [\mkleeneopen{}Val\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}AType\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index