list mapがリストの長さを変えないことを証明する例です

List_map_length.v

Require Import List.
Import ListNotations.

Fixpoint list_map {A B:Type} (f : A -> B) (xs : list A) :=
  match xs with
  | [] => []
  | x :: xs => f x :: list_map f xs
  end.
  
Theorem list_map_length : forall (A B: Type) (f: A -> B) xs,
  length (list_map f xs) = length xs.
Proof.
 induction xs.
 - reflexivity.
 - simpl. now rewrite IHxs.
Qed.