I'm working through Software Foundations, I'm at "Maps" right now. There's an exercise:
Lemma t_update_eq : forall (A : Type) (m : total_map A) x v, (x !-> v ; m) x = v. Proof.
I introduce the variables, unfold and destruct
(x =? x)%string:
Proof. intros. unfold t_update. destruct ((x =? x)%string).
and after that point anything I do generates the error "Expected a single focused goal but 2 goals are focused."
I also tried working on
(x =? x)%string by itself in a separate lemma, which again led to that error.
Lemma fuCK : forall x, (x =? x)%string = true. Proof. intros. destruct ((x =? x)%string ) eqn:E. Abort.
What am I missing?