I’m working through the list exercises of the Lists portion of Logical Foundations (still) and I’ve got to one that I can’t quite finish proving.
Here’s the code:
Theorem eqblist_refl: forall l:natlist, true = eqblist l l. Proof. intros l. induction l as [| n l' IHl']. - simpl. reflexivity. - simpl. rewrite <- IHl'. Qed.
The first half of the induction is proven; it’s the second half that I can’t quite seem to figure out. And this is what I get in the output:
1 subgoal n : nat l' : natlist IHl' : true = eqblist l' l' ______________________________________(1/1) true = (n =? n) && true
For the life of me I can’t figure out how to prove n =? n is true. I mean it seems as if it should be provable by simple reflexivity but that doesn’t seem to do it. Can anyone please give me a small nudge in the correct direction?