proposition: Lemma refine_absConstructor (dom : list Type) (oldConstr : constructorType oldRep dom) : @refineConstructor oldRep newRep AbsR _ oldConstr (absConstructor oldConstr).
proof: Proof. induction dom; simpl in *. - unfold refineConstructor, absConstructor, refine; intros. computes_to_inv; eauto. - intros; eapply IHdom. Qed.
imports: Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTRefinement.Core Fiat.ADTRefinement.SetoidMorphisms Fiat.ADTRefinement.GeneralRefinements