fact: Definition subst_all {A} (f : A → term → term → A) : A → list (term * term) → A := fold_right (fun '(v, v') rest => f rest v v').
imports: Coq.NArith.NArith Coq.FSets.FMaps Coq.micromega.Lia Category.Lib Category.Lib.FMapExt