proposition: Lemma INV'_heap_ignore : ∀ L L₀ L₁, fsubset L (L₀ :|: L₁) → INV' L₀ L₁ (heap_ignore L).
proof: Proof. intros L L₀ L₁ hs h₀ h₁. split. - intros hh ℓ n₀ n₁. eapply hh. apply /negP. intro h. eapply injectSubset in h. 2: eauto. rewrite in_fsetU in h. move: h => /orP [h | h]. + rewrite h in n₀. discriminate. + rewrite h in n₁. discriminate. - intros h ℓ v n₀ n₁ ℓ' n. destruct (ℓ' != ℓ) eqn:e. + rewrite get_set_heap_neq. 2: auto. rewrite get_set_heap_neq. 2: auto. apply h. auto. + move: e => /eqP e. subst. rewrite !get_set_heap_eq. reflexivity. 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)