proposition: Lemma refineADT_Build_ADT_Rep_default Sig oldConstrs oldMeths : refineADT (@Build_ADT Sig oldRep oldConstrs oldMeths) (@Build_ADT Sig newRep (fun idx => absConstructor (oldConstrs idx)) (fun idx => absMethod (oldMeths idx))).
proof: Proof. eapply refineADT_Build_ADT_Rep; eauto. Qed.
imports: Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTRefinement.Core Fiat.ADTRefinement.SetoidMorphisms Fiat.ADTRefinement.GeneralRefinements