fact: Definition N_cast (n m : N) : option (forall P, P n -> P m) := match n, m return option (forall P, P n -> P m) with | N0, N0 => Some (fun P x => x) | Npos p, Npos q => match positive_cast p q with | Some k => Some (fun P => k (fun y => P (Npos y))) | None => None end | _, _ => None end.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList