fact: Fixpoint replace {ps} {T U : Type} (m : member T ps) (v : T) {struct m} : asFunc ps U -> asFunc ps U := match m in member _ ps return asFunc ps U -> asFunc ps U with | MZ _ _ => fun f _ => f v | MN _ m => fun f x => replace m v (f x) end.
imports: Coq.Lists.List ExtLib.Data.Member