proposition: Lemma refineObserverLift {oldRep} : forall (dom : list Type) (cod : option Type) (oldObserver : observerType oldRep dom cod), refineObserver eq oldObserver (liftObserverToMethod oldObserver).
proof: Proof. unfold refineObserver, liftObserverToMethod; induction dom; simpl. - destruct cod; intros. + rewrite H by eauto. intros v Comp_v; computes_to_inv; subst; simpl; eauto. + rewrite H by eauto. intros v Comp_v; computes_to_inv; subst; simpl; eauto. - intros. eapply IHdom with (oldObserver := fun r_o => oldObserver r_o d); intros; subst; eauto. Qed.
imports: Fiat.QueryStructure.Automation.MasterPlan Bedrock.Memory