Step
*
of Lemma
decidable__dset_eq
∀s:DSet. ∀a,b:|s|. Dec(a = b ∈ |s|)
BY
{ ((UnivCD) THENA Auto)
THEN ((RWH (RevLemmaC `assert_of_dset_eq`) 0) THEN Auto) }
Latex:
Latex:
\mforall{}s:DSet. \mforall{}a,b:|s|. Dec(a = b)
By
Latex:
((UnivCD) THENA Auto)
THEN ((RWH (RevLemmaC `assert\_of\_dset\_eq`) 0) THEN Auto)
Home
Index