proposition: Lemma cast_fun_K : ∀ S T f e1 e2, @cast_fun S T S T e1 e2 f = f.
proof: Proof. intros S T f e1 e2. rewrite (uip e1 erefl). rewrite (uip e2 erefl). 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)