proposition: Theorem list_map_app_at : ∀ A B (g : A → B) l x, List.map g l ++ [g x] = List.map g (l ++ [x]).
proof: Proof. intros. induction l as [| b]; [ reflexivity | simpl ]. rewrite IHl; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Psatz