fact: Fixpoint positive_cast (n m : positive) {struct n} : option (forall P, P n -> P m) := match n, m return option (forall P, P n -> P m) with | xH, xH => Some (fun P x => x) | xO p, xO q => match positive_cast p q with | Some k => Some (fun P => k (fun y => P (xO y))) | None => None end | xI p, xI q => match positive_cast p q with | Some k => Some (fun P => k (fun y => P (xI y))) | None => None end | _, _ => None end.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList