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