proposition: Lemma refine_addCacheToConstructor_step (Dom : list Type) (oldConstr : constructorType rep Dom) (newConstr : constructorType cachedRep Dom) : refineConstructor_eq _ (addCacheToConstructor oldConstr) newConstr -> @refineConstructor rep cachedRep cachedRep_AbsR _ oldConstr newConstr.
proof: Proof. eapply refineConstructor_eq_trans; eauto using refine_addCacheToConstructor. Qed.
imports: Fiat.Common Fiat.Computation Fiat.ADT Coq.Sets.Ensembles Fiat.ADTRefinement Fiat.ADTRefinement.Refinements.ADTRepInv