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