proposition: Theorem get_put_eq : forall {T n} (v : vector T n) (f : fin n) val, get f (put f val v) = val.
proof: Proof. induction n. { inversion f. } { remember (S n). destruct f. inversion Heqn0; subst; intros; reflexivity. inversion Heqn0; subst; simpl; auto. } Qed.
imports: ExtLib.Data.Fin