proposition: Lemma refine_addCacheToConstructor (Dom : list Type) (oldConstr : constructorType rep Dom) : @refineConstructor rep cachedRep cachedRep_AbsR _ oldConstr (addCacheToConstructor oldConstr).
proof: Proof. unfold cachedRep_AbsR, refine in *; intros; intuition; subst. induction Dom; simpl. - repeat (f_equiv; intro). computes_to_inv; subst. repeat computes_to_econstructor; eauto. - intros; eapply IHDom. Qed.
imports: Fiat.Common Fiat.Computation Fiat.ADT Coq.Sets.Ensembles Fiat.ADTRefinement Fiat.ADTRefinement.Refinements.ADTRepInv