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