Step
*
1
1
of Lemma
mset_for_wf
1. s : DSet
2. g : IAbMonoid
3. f : |s| ⟶ |g|
4. as : |s| List
5. bs : |s| List
6. as ≡(|s|) bs
⊢ (For{g} x ∈ as. f[x]) = (For{g} x ∈ bs. f[x]) ∈ |g|
BY
{ ((RWH (HypC (-1)) 0) THEN Auto) }
Latex:
Latex:
1.  s  :  DSet
2.  g  :  IAbMonoid
3.  f  :  |s|  {}\mrightarrow{}  |g|
4.  as  :  |s|  List
5.  bs  :  |s|  List
6.  as  \mequiv{}(|s|)  bs
\mvdash{}  (For\{g\}  x  \mmember{}  as.  f[x])  =  (For\{g\}  x  \mmember{}  bs.  f[x])
By
Latex:
((RWH  (HypC  (-1))  0)  THEN  Auto)
Home
Index