proposition: Lemma get_amapi_outofbound : forall {A B} (f:int -> A -> B) t i, i <? length t = false -> (amapi f t).[i] = f (length t) (default t).
proof: Proof. intros A B f t i H1; rewrite get_outofbound. apply default_amapi. rewrite length_amapi; auto. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz