proposition: Lemma refineADT_BuildADT_ReplaceConstructor (Rep : Type) (AbsR : Rep -> Rep -> Prop) {n n'} (consSigs : Vector.t consSig n) (methSigs : Vector.t methSig n') (consDefs : ilist (B := @consDef Rep) consSigs) (methDefs : ilist (B := @methDef Rep) methSigs) (idx : @Fin.t n) (newDef : consDef (Vector.nth consSigs idx)) : (forall consIdx, refineConstructor AbsR (getConsDef consDefs consIdx) (getConsDef consDefs consIdx)) -> (forall methIdx, refineMethod AbsR (getMethDef methDefs methIdx) (getMethDef methDefs methIdx)) -> refineConstructor AbsR (consBody (ith consDefs idx )) (consBody newDef) -> refineADT (BuildADT consDefs methDefs) (ADTReplaceConsDef consDefs methDefs idx newDef).
proof: Proof. intros; eapply refineADT_BuildADT_Rep with (AbsR := AbsR); eauto. intros; unfold getConsDef. unfold replaceConsDef. destruct (fin_eq_dec consIdx idx); subst. rewrite ith_replace_Index_eq; eauto. rewrite ith_replace_Index_neq; eauto. Qed.
imports: Coq.Lists.List Coq.Arith.Arith Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADT.ComputationalADT Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.IterateBoundedIndex Fiat.ADTNotation.BuildADTSig Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildComputationalADT Fiat.ADTNotation.BuildADTReplaceMethods Fiat.ADTRefinement.Core Fiat.ADTRefinement.GeneralRefinements Fiat.ADTRefinement.SetoidMorphisms Fiat.ADTRefinement.BuildADTSetoidMorphisms Coq.Strings.String