proposition: Lemma length_or_of_imp : forall args, PArray.length (or_of_imp args) = PArray.length args.
proof: Proof. intro; unfold or_of_imp; apply length_amapi. Qed.
imports: PArray List Bool ZArith Psatz Misc State SMT_terms BVList