proposition: Lemma noMoreLets : forall f1 f2 : OrdCat⦅ J AA ; W BB ⦆, f1 = f2 -> (let (a,_) := dnib W f1 in a) = (let (a,_) := dnib W f2 in a).
proof: Proof. move=> f1 f2. move=> Hf. rewrite Hf. reflexivity. Qed.
imports: Coq(Morphisms) mathcomp(all_ssreflect) Mon(SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(OrderEnrichedRelativeAdjunctions OrderEnrichedRelativeAdjunctionsExamples ChoiceAsOrd)