proposition: Lemma rel_jdg_replace : ∀ (A B : choiceType) (pre : precond) (post : postcond A B) l l' r r', ⊢ ⦃ pre ⦄ l ≈ r ⦃ post ⦄ → l = l' → r = r' → ⊢ ⦃ pre ⦄ l' ≈ r' ⦃ post ⦄.
proof: Proof. intros A B pre post l l' r r' h ? ?. subst. auto. Qed.
imports: mathcomp(all_ssreflect all_algebra reals distr fingroup.fingroup realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) extructures(ord fset fmap) Crypt(Axioms Prelude pkg_core_definition pkg_composition pkg_notation RulesStateProb pkg_advantage pkg_lookup pkg_semantics pkg_heap pkg_invariants pkg_distr pkg_rhl pkg_tactics choice_type) Coq(Utf8 FunctionalExtensionality Setoids.Setoid Classes.Morphisms) Equations(Equations)