proposition: Lemma refineADT_BuildADT_Rep_default {n n'} {consSigs : Vector.t consSig n} {methSigs : Vector.t methSig n'} (consDefs : ilist (B := @consDef oldRep) consSigs) (methDefs : ilist (B := @methDef oldRep) methSigs) : refineADT (BuildADT consDefs methDefs) (BuildADT (imap absConsDef consDefs) (imap absMethDef methDefs)).
proof: Proof. eapply refineADT_Build_ADT_Rep with (AbsR := AbsR); eauto; intros. - unfold getConsDef. rewrite <- ith_imap. apply refine_absConstructor. - unfold getMethDef. rewrite <- ith_imap. apply refine_absMethod. Qed.
imports: Coq.Lists.List Fiat.Common Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.Common.IterateBoundedIndex Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTNotation.BuildADTSig Fiat.ADTNotation.BuildADT Fiat.ADTRefinement.Core Fiat.ADTRefinement.SetoidMorphisms Fiat.ADTRefinement.GeneralRefinements Fiat.ADTRefinement.GeneralBuildADTRefinements Fiat.ADTRefinement.Refinements.HoneRepresentation Fiat.ADTRefinement.BuildADTSetoidMorphisms