proposition: Lemma code_ext : ∀ A (u v : code A), u.(prog) = v.(prog) → u = v.
proof: Proof. intros A u v h. destruct u as [u hu], v as [v hv]. cbn in h. subst. f_equal. apply proof_irrelevance. Qed.
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)