fact: Definition refineMethod {dom : list Type} {cod : option Type} (oldMethod : methodType oldRep dom cod) (newMethod : methodType newRep dom cod) := forall r_o r_n, r_o ≃ r_n -> @refineMethod' dom cod (oldMethod r_o) (newMethod r_n).
imports: Fiat.Common Fiat.Computation Fiat.ADT Coq.Sets.Ensembles