proposition: Lemma get_outofbound : forall A (t:array A) i, (i <? length t) = false -> t.[i] = default t.
proof: Proof. intros A t i; unfold get. destruct t as ((t, d), l). unfold length; intro Hi; rewrite Hi; clear Hi. reflexivity. Qed.
imports: Int63 Psatz ZArith