proposition: Theorem nth_listReplace_eq : forall (A : Set) i (ls : list A) a def1 def2, nth i (listReplace ls i a def1) def2 = a.
proof: Proof. induction i; destruct ls; intuition; simpl in *. eapply nth_listReplace_nil_eq. eauto. Qed.
imports: FCF.FCF Permutation