proposition: Lemma refineADT_Build_ADT_Both rep Sig : forall ms ms', (forall idx, @refineMethod _ _ eq (fst (MethodDomCod Sig idx)) (snd (MethodDomCod Sig idx)) (ms idx) (ms' idx)) -> forall cs cs', (forall idx, @refineConstructor _ _ eq (ConstructorDom Sig idx) (cs idx) (cs' idx)) -> refineADT (@Build_ADT Sig rep cs ms) (@Build_ADT Sig rep cs' ms').
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