I have a lemma that says, $"$if an integer i is a member of a singleton set s then s $=\{$i$\}."$ I write this lemma as follows:

lemma LemIAmSingle$($s:set, i:int$)$ ensures $|$s$|==1$ && i in s $==>$ s$==\{$i$\}\{\}$

This generates an error because Dafny is not able to prove this property. Which of the following can be used as proof?

$($a$)$

assert i in s $==>|$s $-\{$i$\}|==0$

$($b$)$

assert $(|$s$|==1$ && i in s$)==>|$s $-\{$i$\}|==0$

$($c$)$

assert $|$s $-\{$i$\}|==0$

$($d$)$

if $|$s$|==1\{$ assert i in s $==>|$s $-\{$i$\}|==0$; $\}$

$($e$)$

if $|$s$|==1$ && i in s $\{$ assert $|$s $-\{$i$\}|==0$; $\}$

$($f$)$

if $|$s$|==1$ && i in s && $|$s $-\{$i$\}|==0\{$ assert true; $\}$