proposition: Lemma refineADT_BuildADT_Both rep n n' consigs methSigs : forall oldCons newCons, (forall consIdx, @refineConstructor _ _ eq _ (getConsDef oldCons consIdx) (getConsDef newCons consIdx)) -> forall oldMeth newMeth, (forall methIdx, @refineMethod _ _ eq _ _ (getMethDef oldMeth methIdx) (getMethDef newMeth methIdx)) -> refineADT (@BuildADT n n' rep consigs methSigs oldCons oldMeth) (@BuildADT n n' rep consigs methSigs newCons newMeth).
proof: Proof. intros; eapply refineADT_BuildADT_Rep; eauto; reflexivity. Qed.
imports: Fiat.Common Fiat.ADTNotation.BuildADT Fiat.ADTRefinement.Core Fiat.ADTRefinement.SetoidMorphisms