Step
*
of Lemma
mset_count_inj
∀s:DSet. ∀a,x:|s|. ((x #∈ mset_inj{s}(a)) = b2i(a (=b) x) ∈ ℤ)
BY
{ ((RepD) THENA Auto) }
1
1. s : DSet
2. a : |s|
3. x : |s|
⊢ (x #∈ mset_inj{s}(a)) = b2i(a (=b) x) ∈ ℤ
Latex:
Latex:
\mforall{}s:DSet. \mforall{}a,x:|s|. ((x \#\mmember{} mset\_inj\{s\}(a)) = b2i(a (=\msubb{}) x))
By
Latex:
((RepD) THENA Auto)
Home
Index