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