fact: Fixpoint UnConstryQueryStructure_Abstract_AbsR' {n} {qsSchema} (r_o : ilist2 (B := (fun ns : RawSchema => RawUnConstrRelation (rawSchemaHeading ns))) qsSchema) (r_n : Iterate_Dep_Type_BoundedIndex (fun idx : Fin.t n=> @IndexedEnsemble (@RawTuple (rawSchemaHeading (Vector.nth qsSchema idx))))) : Prop := match qsSchema as qsSchema return forall (r_o : ilist2 (B := (fun ns : RawSchema => RawUnConstrRelation (rawSchemaHeading ns))) qsSchema) (r_n : Iterate_Dep_Type_BoundedIndex (fun idx : Fin.t _ => @IndexedEnsemble (@RawTuple (rawSchemaHeading (Vector.nth qsSchema idx))))), Prop with | Vector.cons sch _ qsSchema' => fun r_o r_n => ilist2_hd r_o = prim_fst r_n /\ UnConstryQueryStructure_Abstract_AbsR' (prim_snd r_o) (prim_snd r_n) | Vector.nil => fun _ _ => True end r_o r_n.
imports: Fiat.QueryStructure.Automation.MasterPlan Bedrock.Memory