This is an exercise from Software foundations for my discrete math & functional programming class. I am a little stuck with the end of the code because it works for the first two examples but it doesn't work for my false case and I can't figure out why...

(** **** Exercise: 2 stars, standard (eqblist)

Fill in the definition of [eqblist], which compares

lists of numbers for equality. Prove that [eqblist l l]

yields [true] for every list [l]. *)

Fixpoint eqblist (l1 l2 : natlist) : bool :=

match l1, l2 with

| nil, nil => true

| (h1 :: t1), (h2 :: t2) => true

| _,_ => false

end.

Example test_eqblist1 :

(eqblist nil nil = true).

Proof. reflexivity. Qed. (works)

Example test_eqblist2 :

eqblist [1;2;3] [1;2;3] = true.

Proof. reflexivity. Qed. (works)

Example test_eqblist3 :

eqblist [1;2;3] [1;2;4] = false.

Proof. reflexivity. Qed. (this one doesn't work! )