proposition: Lemma listReplace_twice_nil : forall (A : Set)(n : nat) (a1 a2 def : A), listReplace (listReplace nil n a1 def) n a2 def = listReplace nil n a2 def.
proof: Proof. induction n; intuition; simpl in *. f_equal. eapply IHn. Qed.
imports: FCF.FCF Permutation