proposition: Lemma BuildGetMessageMethodID_ibound {n''} (subtopics' : Vector.t (Fin.t n) n'') : forall (idx : Fin.t n''), Vector.nth (Vector.map methID (MessageSigs' subtopics')) (Fin.depair idx Fin.F1) = ("Get" ++ 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.Common.ilist2 Fiat.ADT Fiat.ADT.ComputationalADT Fiat.ADTNotation Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements Fiat.Fiat4Monitors.RADL_Topics