proposition: Lemma BuildSetFlagsMethodID_ibound {n'} (subtopics : Vector.t (Fin.t n) n') : forall (idx : Fin.t n'), Vector.nth (Vector.map methID (FlagsSigs subtopics)) (Fin.depair idx (Fin.FS Fin.F1)) = ("Set" ++ Vector.nth TopicNames (Vector.nth subtopics idx))%string.
proof: Proof. induction subtopics. - intro; inversion idx. - intro; revert subtopics IHsubtopics; pattern n0, idx. eapply Fin.rectS; simpl; intros; eauto. Qed.
imports: Coq.Strings.String Coq.Bool.Bool Coq.Lists.List Coq.Arith.Arith Coq.Program.Program Fiat.ADT Fiat.ADT.ComputationalADT Fiat.ADTNotation Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements Fiat.Fiat4Monitors.RADL_Topics Fiat.Fiat4Monitors.RADL_Flag Bedrock.Memory