proposition: Lemma preserve_update_triple_rhs_lookup : ∀ ℓ₁ ℓ₂ ℓ₃ (R : _ → _ → _ → Prop) v₁ v₂ v₃ (l : seq heap_val) m, lookup_hpv_r ℓ₁ l = Some v₁ → lookup_hpv_r ℓ₂ l = Some v₂ → lookup_hpv_r ℓ₃ l = Some v₃ → R v₁ v₂ v₃ → preserve_update_mem l m (triple_rhs ℓ₁ ℓ₂ ℓ₃ R).
proof: Proof. intros ℓ₁ ℓ₂ ℓ₃ R v₁ v₂ v₃ l m h₁ h₂ h₃ h. intros s₀ s₁ hh. unfold triple_rhs in *. destruct update_heaps eqn:e. erewrite lookup_hpv_r_spec. 2,3: eauto. erewrite lookup_hpv_r_spec. 2,3: eauto. erewrite lookup_hpv_r_spec. 2,3: eauto. auto. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap pkg_semantics pkg_lookup pkg_advantage) Equations.Prop.DepElim Equations(Equations) Crypt(FreeProbProg)