fact: Fixpoint FlagsDefs' {m} (subtopics'' : Vector.t (Fin.t n) m) {n''} (subtopics' : Vector.t (Fin.t n) n'') : (forall (topic : Fin.t n''), cMethDef (Rep := Flags subtopics'') (GetFlagSig (Vector.nth subtopics' topic))) -> (forall (topic : Fin.t n''), cMethDef (Rep := Flags subtopics'') (SetFlagSig (Vector.nth subtopics' topic))) -> ilist (B := cMethDef (Rep := Flags subtopics'')) (FlagsSigs subtopics') := match subtopics' in Vector.t _ n'' return (forall (topic : Fin.t n''), cMethDef (Rep := Flags subtopics'') (GetFlagSig (Vector.nth subtopics' topic))) -> (forall (topic : Fin.t n''), cMethDef (Rep := Flags subtopics'') (SetFlagSig (Vector.nth subtopics' topic))) -> ilist (B := cMethDef (Rep := Flags subtopics'')) (FlagsSigs subtopics') with | Vector.nil => fun _ _ => tt | Vector.cons _ n0 subtopics' => fun GetFlagDef SetFlagDef => Build_prim_prod (GetFlagDef Fin.F1) (Build_prim_prod (SetFlagDef Fin.F1) (@FlagsDefs' _ subtopics'' _ subtopics' (fun t => GetFlagDef (Fin.FS t)) (fun t => SetFlagDef (Fin.FS t)))) end.
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