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