proposition: Lemma positive_cast_refl: forall p, positive_cast p p = Some (fun P (H : P p) => H).
proof: Proof. induction p as [p IHp|p IHp| ]; simpl; try rewrite IHp; auto. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList