proposition: Lemma lookup_op_spec : ∀ p o f, lookup_op p o = Some f → p (ide o) = Some (chsrc o ; chtgt o ; f).
proof: Proof. intros p o f e. destruct o as [id [S T]]. cbn in *. destruct (p id) as [[S' [T' g]]|] eqn:e1. 2: discriminate. destruct choice_type_eqP. 2: discriminate. destruct choice_type_eqP. 2: discriminate. noconf e. subst. reflexivity. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssreflect eqtype choice seq ssrfun ssrbool ssrnat) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd StateTransformingLaxMorph choice_type pkg_core_definition RulesStateProb) Equations(Equations)