proposition: Lemma refineADT_BuildADT_Rep_refine_All_eq {n n'} (consSigs : Vector.t consSig n) (methSigs : Vector.t methSig n') (consDefs : ilist (B := @consDef Rep) consSigs) (methDefs : ilist (B := @methDef Rep) methSigs) (refined_consDefs : ilist (B := @consDef Rep) consSigs) (refined_methDefs : ilist (B := @methDef Rep) methSigs) : Iterate_Ensemble_BoundedIndex (fun idx => refineConstructor_eq _ (ith consDefs idx) (ith refined_consDefs idx)) -> Iterate_Ensemble_BoundedIndex (fun idx => refineMethod_eq (ith methDefs idx) (ith refined_methDefs idx)) -> refineADT (BuildADT consDefs methDefs) (BuildADT refined_consDefs refined_methDefs).
proof: Proof. intros; eapply refineADT_BuildADT_Rep_refine_All with (AbsR := eq). - revert H; clear; induction consSigs; simpl in *; destruct consDefs; destruct refined_consDefs; try econstructor; simpl. intros; destruct H; destruct prim_fst; destruct prim_fst0; econstructor; eauto. destruct h; eapply (@refineConstructor_eq_sound consDom); eauto. - revert H0; clear; induction methSigs; simpl in *; destruct methDefs; destruct refined_methDefs; try econstructor; simpl. intros; destruct H0; destruct prim_fst; destruct prim_fst0; econstructor; eauto. destruct h; eapply (@refineMethod_eq_sound methDom methCod); eauto. Qed.
imports: Coq.Lists.List Fiat.Common Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.Common.IterateBoundedIndex Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTNotation.BuildADTSig Fiat.ADTNotation.BuildADT Fiat.ADTRefinement.Core Fiat.ADTRefinement.SetoidMorphisms Fiat.ADTRefinement.GeneralRefinements Fiat.ADTRefinement.GeneralBuildADTRefinements Fiat.ADTRefinement.BuildADTRefinements.HoneRepresentation Fiat.ADTRefinement.BuildADTSetoidMorphisms