proposition: Lemma listReplace_in : forall (A : Set)(ls : list A)(a1 a2 def : A)(i : nat), In a1 (listReplace ls i a2 def) -> (In a1 ls \/ a1 = a2 \/ a1 = def).
proof: Proof. induction ls; intuition; simpl in *. right. eapply listReplace_in_nil. eauto. destruct i; simpl in *. intuition. intuition. edestruct (IHls); eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation