proposition: Lemma get_or_of_imp2 : forall args i, 0 <? PArray.length args -> i = (PArray.length args) - 1 -> (or_of_imp args).[i] = args.[i].
proof: Proof. unfold or_of_imp; intros args i Heq Hi; rewrite get_amapi; subst i. rewrite Int63.eqb_refl; auto. rewrite ltb_spec, (to_Z_sub_1 _ _ Heq); lia. Qed.
imports: PArray List Bool ZArith Psatz Misc State SMT_terms BVList