proposition: Lemma put_pre_cond_loc_rel : ∀ ℓ v l (R : locRel l), ℓ \notin (map fst l) → put_pre_cond ℓ v (loc_rel l R).
proof: Proof. intros ℓ v l R h s₀ s₁ hc. unfold loc_rel in *. induction l as [| [ℓ' si] l ih]. - assumption. - simpl. simpl in h. simpl in hc. rewrite notin_cons in h. move: h => /andP [hn h]. apply ih. + assumption. + destruct si. all: rewrite !get_set_heap_neq. 1,3: auto. all: rewrite eq_sym. all: 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)