proposition: Theorem refineADT_BuildADT_Rep n n' consSigs methSigs oldRep newRep (AbsR : oldRep -> newRep -> Prop) : @respectful_heteroT _ _ _ _ (fun oldCons newCons => forall consIdx, @refineConstructor oldRep newRep AbsR _ (getConsDef oldCons consIdx) (getConsDef newCons consIdx)) (fun x y => @respectful_heteroT _ _ _ _ (fun oldMeth newMeth => forall methIdx, @refineMethod oldRep newRep AbsR _ _ (getMethDef oldMeth methIdx) (getMethDef newMeth methIdx)) (fun m m' => refineADT)) (@BuildADT oldRep n n' consSigs methSigs) (@BuildADT newRep n n' consSigs methSigs).
proof: Proof. unfold Proper, respectful_heteroT; intros. let A := match goal with |- refineADT ?A ?B => constr:(A) end in let B := match goal with |- refineADT ?A ?B => constr:(B) end in eapply (@refinesADT _ A B AbsR); unfold id, pointwise_relation in *; simpl in *; intros; eauto. Qed.
imports: Fiat.Common Fiat.ADTNotation.BuildADT Fiat.ADTRefinement.Core Fiat.ADTRefinement.SetoidMorphisms