fact: Fixpoint fromMethod' {rep : Type} {dom : list Type} : forall {cod : option Type}, methodType' rep dom cod -> rep -> Prop := match dom return forall {cod : option Type}, methodType' rep dom cod -> rep -> Prop with | [ ] => fun cod => match cod return methodType' rep [ ] cod -> rep -> Prop with | None => fun meth r => computes_to meth r | Some C => fun meth r => exists c : C, computes_to meth (r, c) end | D :: dom' => fun cod meth r => exists d, fromMethod' (meth d) r end.
imports: Fiat.ADT Fiat.ADTNotation Coq.Sets.Ensembles Coq.Lists.List