fact: Fixpoint cast (A B: type) : cast_result A B := match A as C, B as D return cast_result C D with | Tindex i, Tindex j => match N_cast i j with | Some k => Cast (fun P => k (fun y => P (Tindex y))) | None => NoCast end | TZ, TZ => idcast | Tbool, Tbool => idcast | Tpositive, Tpositive => idcast | TBV n, TBV m => match N_cast n m with | Some k => Cast (fun P => k (fun y => P (TBV y))) | None => NoCast end | TFArray k1 e1, TFArray k2 e2 => match cast k1 k2, cast e1 e2 with | Cast kk, Cast ke => let ka P := let Pb d := P (TFArray d e1) in let Pc d := P (TFArray k2 d) in fun x => ke Pc (kk Pb x) in Cast ka | _, _ => NoCast end | _, _ => NoCast end.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList