proposition: Lemma refineConstructor_eq_sound : forall cSig (cDef refinedCDef : constructorType Rep cSig), refineConstructor_eq Rep cDef refinedCDef -> let H := refinedCDef in refineConstructor eq cDef H.
proof: Proof. induction cSig; simpl; intros. - etransitivity. + apply refine_under_bind; intros. refine pick val a; eauto; finish honing. + simpl; autorewrite with monad laws; eauto. - eapply IHcSig; 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.BuildADTRefinements.HoneRepresentation Fiat.ADTRefinement.BuildADTSetoidMorphisms