proposition: Lemma BuildSetTupleMethodID_ibound {n'} (HeadingTypes : Vector.t Type n') (HeadingNames : Vector.t string n') : forall (idx : Fin.t n'), Vector.nth (Vector.map methID (TupleSigs' HeadingTypes HeadingNames)) (Fin.depair idx (Fin.FS Fin.F1)) = ("Set" ++ Vector.nth HeadingNames idx)%string.
proof: Proof. pattern n', HeadingTypes, HeadingNames. eapply Vector.rect2. - intro; inversion idx. - intros; generalize dependent idx; intro; revert v1 v2 H. pattern n, idx. eapply Fin.rectS; simpl; intros; eauto. Qed.
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.Heading Fiat.QueryStructure.Specification.Representation.Tuple