proposition: Lemma get_amap_outofbound : forall {A B} (f:A -> B) t i, i <? length t = false -> (amap f t).[i] = f (default t).
proof: Proof. intros; unfold amap; apply get_amapi_outofbound; assumption. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz