proposition: Lemma refineADT_Build_ADT_RepInv Sig : forall constr constr', (forall idx, @refineConstructor _ _ repInvAbsR (ConstructorDom Sig idx) (constr idx) (constr' idx)) -> forall meth meth', (forall idx, @refineMethod _ _ repInvAbsR (fst (MethodDomCod Sig idx)) (snd (MethodDomCod Sig idx)) (meth idx) (meth' idx)) -> refineADT (@Build_ADT Sig rep constr meth) (@Build_ADT Sig rep constr' meth').
proof: Proof. intros; eapply refineADT_Build_ADT_Rep; eauto; reflexivity. Qed.
imports: Fiat.Common Fiat.Computation Coq.Sets.Ensembles Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTRefinement.Core Fiat.ADTRefinement.SetoidMorphisms Fiat.ADTRefinement.GeneralRefinements