fact: Definition Tuple2Defs' {n'} (HeadingTypes : Vector.t Type n') (HeadingNames2 : Vector.t string n') : (forall (attr : Fin.t n'), cMethDef (Rep := @Tuple2 heading) (GetTuple2Sig (Vector.nth HeadingNames2 attr) (Vector.nth HeadingTypes attr))) -> (forall (attr : Fin.t n'), cMethDef (Rep := @Tuple2 heading) (SetTuple2Sig (Vector.nth HeadingNames2 attr) (Vector.nth HeadingTypes attr))) -> ilist (B := cMethDef (Rep := @Tuple2 heading)) (Tuple2Sigs' HeadingTypes HeadingNames2) := Vector.rect2 (fun n HeadingTypes HeadingNames2 => (forall (attr : Fin.t n), cMethDef (Rep := @Tuple2 heading) (GetTuple2Sig (Vector.nth HeadingNames2 attr) (Vector.nth HeadingTypes attr))) -> (forall (attr : Fin.t n), cMethDef (Rep := @Tuple2 heading) (SetTuple2Sig (Vector.nth HeadingNames2 attr) (Vector.nth HeadingTypes attr))) -> ilist (n := n * 2) (B := cMethDef (Rep := @Tuple2 heading)) (Tuple2Sigs' HeadingTypes HeadingNames2)) (fun _ _ => ()) (fun n HeadingTypes HeadingNames2 Tuple2Defs' aType id GetTuple2Def' SetTuple2Def' => icons (GetTuple2Def' Fin.F1) (icons (SetTuple2Def' Fin.F1) (Tuple2Defs' (fun n => GetTuple2Def' (Fin.FS n)) (fun n => SetTuple2Def' (Fin.FS n))))) HeadingTypes HeadingNames2.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.ZArith.ZArith Fiat.Common.ilist2 Fiat.Common.StringBound Fiat.ADT Fiat.ADT.ComputationalADT Fiat.ADTNotation Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading2 Fiat.QueryStructure.Specification.Representation.Tuple2