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