proposition: Theorem get_put_neq : forall {T n} (v : vector T n) (f f' : fin n) val, f <> f' -> get f (put f' val v) = get f v.
proof: Proof. induction n. { inversion f. } { remember (S n); destruct f. { inversion Heqn0; clear Heqn0; subst; intros. destruct (fin_case f'); try congruence. destruct H0; subst. auto. } { inversion Heqn0; clear Heqn0; subst; intros. destruct (fin_case f'). subst; auto. destruct H0; subst. simpl. eapply IHn. congruence. } } Qed.
imports: ExtLib.Data.Fin