proposition: Lemma default_copy A (t:array A) : default (copy t) = default t.
proof: Proof. assert (irr_lt : length t <? length t = false). { destruct (Uint63.ltbP (length t) (length t)); try reflexivity. exfalso; eapply BinInt.Z.lt_irrefl; eassumption. } assert (get_copy := get_copy A t (length t)). rewrite !get_out_of_bounds in get_copy; try assumption. rewrite length_copy; assumption. Qed.
imports: Uint63