proposition: Lemma prove_code : ∀ {A} (P : code A → Type) p q, P p → p.(prog) = q.(prog) → P q.
proof: Proof. intros A P p q h e. apply code_ext in e. subst. auto. Defined.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssreflect eqtype choice seq ssrfun ssrbool) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd RulesStateProb StateTransformingLaxMorph choice_type) Equations.Prop.DepElim Equations(Equations)