fact: Fixpoint liftObserverToMethod' (rep : Type) (dom : list Type) (cod : option Type) (observer : observerType' rep dom cod) (r : rep) {struct dom} : methodType' rep dom cod := match dom as dom' return observerType' rep dom' cod -> methodType' rep dom' cod with | [] => match cod as cod' return observerType' rep [ ] cod' -> methodType' rep [ ] cod' with | Some cod' => fun observer => r' <- observer; ret (r, r') | None => fun observer => r' <- observer; ret r end | D :: dom' => fun observer' (d : D) => liftObserverToMethod' dom' cod (observer' d) r end observer.
imports: Fiat.QueryStructure.Automation.MasterPlan Bedrock.Memory