Step
*
of Lemma
mset_inj_wf_f
∀s:DSet. ∀x:|s|. (mset_inj{s}(x) ∈ FiniteSet{s})
BY
{ TACTIC:(Auto THEN MemTypeCD THEN Auto) }
1
1. s : DSet
2. x : |s|
3. x@0 : |s|
⊢ (x@0 #∈ mset_inj{s}(x)) ≤ 1
Latex:
Latex:
\mforall{}s:DSet. \mforall{}x:|s|. (mset\_inj\{s\}(x) \mmember{} FiniteSet\{s\})
By
Latex:
TACTIC:(Auto THEN MemTypeCD THEN Auto)
Home
Index