Step
*
1
of Lemma
dset_eq_refl
1. s : DSet
2. a : |s|
⊢ ↑(a (=
b
) a)
BY
{ ((RW bool_to_propC 0) THEN Auto) }
Latex:
Latex:
1. s : DSet
2. a : |s|
\mvdash{} \muparrow{}(a (=\msubb{}) a)
By
Latex:
((RW bool\_to\_propC 0) THEN Auto)
Home
Index