proposition: Lemma mkprog_rewrite : ∀ {L I A T} {x y} (p : T → _) h (e : x = y), @mkprog L I A (p x) h = mkprog (p y) (sig_rewrite_aux p h e).
proof: Proof. intros L I A T x y p h e. subst. reflexivity. 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)