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