proposition: Lemma get_set_same_default A (t : array A) (i : int) : t.[i <- default t].[i] = default t.
proof: Proof. case_eq (i <? length t); intros. - rewrite get_set_same; trivial. - rewrite get_out_of_bounds, default_set; trivial. rewrite length_set; trivial. Qed.
imports: Uint63