proposition: Lemma list_map_size_spec (g : A -> B) (l : list A) : list_map_size l (fun x _ => g x) = List.map g l.
proof: Proof. funelim (list_map_size l (λ (x : A) (_ : f x < list_size l), g x)); simpl; trivial. now rewrite H. Qed.
imports: Equations(Equations) Lia Utf8 List