fact: Fixpoint refineMethod_eq' {dom : list Type} {cod : option Type} : methodType' oldRep dom cod -> methodType' oldRep dom cod -> Prop := match dom return methodType' oldRep dom cod -> methodType' oldRep dom cod -> Prop with | nil => match cod return methodType' oldRep [] cod -> methodType' oldRep [] cod -> Prop with | Some cod' => fun oldMethod newMethod => refine oldMethod newMethod | _ => fun oldMethod newMethod => refine oldMethod newMethod end | cons D dom' => fun oldMethod newMethod => forall d : D, @refineMethod_eq' dom' cod (oldMethod d) (newMethod d) end.
imports: Fiat.Common Fiat.Computation Fiat.ADT Coq.Sets.Ensembles