fact: Fixpoint listReplace (ls : list A)(i : nat)(a def : A) := match i with | O => match ls with | nil => a :: nil | a' :: ls' => a :: ls' end | S i' => match ls with | nil => def :: (listReplace nil i' a def) | a' :: ls' => a' :: (listReplace ls' i' a def) end end.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool