proposition: Lemma refine_AbsConstructor : forall Dom (oldConstructor : constructorType _ Dom) refinedConstructor, (refineConstructor AbsR oldConstructor refinedConstructor) -> refineConstructor eq (absConstructor AbsR oldConstructor) refinedConstructor.
proof: Proof. unfold refineMethod; intros; subst. induction Dom; simpl; intros. - intros v ComputesTo_v; subst. refine pick val v; eauto. apply H in ComputesTo_v; computes_to_inv; subst. eexists; split; eauto. - eapply IHDom; eauto. 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