proposition: Lemma refineADT_Build_ADT_Constructors rep Sig ms : 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