fact: Definition override {V: Type} (m: nat -> V) (k: nat) (v: V): nat -> V := fun (k': nat) => if (eq_nat_dec k' k) then v else (m k').
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)