proposition: Corollary SharpenStep_BuildADT_ReplaceConstructor_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 : consDef (Vector.nth consSigs idx)) adt'' : (let H := consBody newDef in refineConstructor eq (consBody (ith consDefs idx)) H) -> refineADT (ADTReplaceConsDef consDefs methDefs idx newDef) adt'' -> refineADT (BuildADT consDefs methDefs) adt''.
proof: Proof. intros; eapply SharpenStep; try exact X. eapply refineADT_BuildADT_ReplaceConstructor with (AbsR := eq); simpl; unfold refine; intros; subst; eauto. - reflexivity. - reflexivity. 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