The problem of functional language: Coq. Need to use coq code to solve the below question.

You can use function fold to define the length of the list as follows:

Definition fold_length {X : Type} (l : list X) : nat :=

fold (fun _ n => S n) l 0.

Prove that fold_length and length compute the same value for any arbitrary list.