fact: Fixpoint Iterate_Dep_Type_AbsR {n} (A B : Fin.t n -> Type) (AB_AbsR : forall idx, A idx -> B idx -> Prop) (a : Iterate_Dep_Type_BoundedIndex A) (b : Iterate_Dep_Type_BoundedIndex B) : Prop := match n as n' return forall (A B : Fin.t n' -> Type) (AB_AbsR : forall idx, A idx -> B idx -> Prop), Iterate_Dep_Type_BoundedIndex A -> Iterate_Dep_Type_BoundedIndex B -> Prop with | S n' => fun A B AB_AbsR a b => AB_AbsR _ (prim_fst a) (prim_fst b) /\ Iterate_Dep_Type_AbsR (fun n' => A (Fin.FS n')) (fun n' => B (Fin.FS n')) (fun n' => AB_AbsR (Fin.FS n')) (prim_snd a) (prim_snd b) | _ => fun _ _ _ _ _ => True end A B AB_AbsR a b.
imports: Fiat.QueryStructure.Automation.MasterPlan Bedrock.Memory