proposition: Lemma length_update : forall n v l, length (update n v l) = length l.
proof: Proof. Proof using. intros. gen n. induction l; intros. { auto. } { destruct n as [|n']. { rewrite update_zero. rew_list~. } { rewrite update_succ. rew_list. rewrite~ IHl. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)