proposition: Lemma preserve_update_triple_rhs_lookup_None : ∀ ℓ₁ ℓ₂ ℓ₃ (R : _ → _ → _ → Prop) (l : seq heap_val) m, lookup_hpv_r ℓ₁ l = None → lookup_hpv_r ℓ₂ l = None → lookup_hpv_r ℓ₃ l = None → preserve_update_mem l m (triple_rhs ℓ₁ ℓ₂ ℓ₃ R).
proof: Proof. intros ℓ₁ ℓ₂ ℓ₃ R l m h₁ h₂ h₃. intros s₀ s₁ hh. unfold triple_rhs in *. destruct update_heaps eqn:e. erewrite lookup_hpv_r_None_spec. 2,3: eauto. erewrite lookup_hpv_r_None_spec with (ℓ := ℓ₂). 2,3: eauto. erewrite lookup_hpv_r_None_spec with (ℓ := ℓ₃). 2,3: eauto. eapply remember_pre_pre in hh. 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)