proposition: Lemma FullySharpenStep_BuildADT_ReplaceMethod_eq (Rep : Type) {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 : methDef (Vector.nth methSigs idx)) adt'' : (let H := methBody newDef in refineMethod eq (methBody (ith methDefs idx)) newDef) -> FullySharpenedUnderDelegates (ADTReplaceMethDef consDefs methDefs idx newDef) adt'' -> FullySharpenedUnderDelegates (BuildADT consDefs methDefs) adt''.
proof: Proof. intros; eapply FullySharpenStep. eapply refineADT_BuildADT_ReplaceMethod with (AbsR := eq); simpl; unfold refine; intros; subst; eauto; reflexivity. exact X. 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