fact: Definition ADTReplaceMethDef (idx : Fin.t n') (newDef : methDef (Vector.nth methSigs idx)) : ADT (BuildADTSig consSigs methSigs) := BuildADT consDefs (replaceMethDef idx newDef).
imports: Coq.Lists.List Coq.Strings.String Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.Common Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.ADTNotation.BuildADTSig Fiat.ADTNotation.BuildADT