proposition: Theorem listReplace_length : forall (A : Set)(ls : list A)(i : nat)(a def : A), i < length ls -> length (listReplace ls i a def) = length ls.
proof: Proof. induction ls; intuition; simpl in *. lia. destruct i; simpl in *. trivial. f_equal. eapply IHls. lia. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation