Step
*
of Lemma
comb_for_mset_for_wf
λs,g,f,a,z. (msFor{g} x ∈ a. f[x]) ∈ s:DSet ⟶ g:IAbMonoid ⟶ f:(|s| ⟶ |g|) ⟶ a:MSet{s} ⟶ (↓True) ⟶ |g|
BY
{ ProveOpCombTyping `mset_for_wf` }
Latex:
Latex:
\mlambda{}s,g,f,a,z. (msFor\{g\} x \mmember{} a. f[x]) \mmember{} s:DSet {}\mrightarrow{} g:IAbMonoid {}\mrightarrow{} f:(|s| {}\mrightarrow{} |g|) {}\mrightarrow{} a:MSet\{s\} {}\mrightarrow{} (\mdownarrow{}True)\000C {}\mrightarrow{} |g|
By
Latex:
ProveOpCombTyping `mset\_for\_wf`
Home
Index