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?