proposition: Lemma choice_type_eqP : Equality.axiom choice_type_eq.
proof: Proof. move=> x y. induction x as [ | | | x1 ih1 x2 ih2 | x1 ih1 x2 ih2 | x1 ih1 | x1] in y |- *. all: destruct y as [ | | | y1 y2 | y1 y2 | y1 | y1]. all: simpl. all: try solve [ right ; discriminate ]. all: try solve [ left ; reflexivity ]. - destruct (ih1 y1), (ih2 y2). all: simpl. all: subst. all: try solve [ right ; congruence ]. left. reflexivity. - destruct (ih1 y1), (ih2 y2). all: simpl. all: subst. all: try solve [ right ; congruence ]. left. reflexivity. - destruct (ih1 y1). all: subst. + left. reflexivity. + right. congruence. - destruct (x1 == y1) eqn:e. + move: e => /eqP e. subst. left. reflexivity. + move: e => /eqP e. right. intro h. apply e. inversion h. reflexivity. Qed.
imports: Coq(Utf8 Lia) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples GenericRulesSimple) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr realsum seq all_algebra fintype) Crypt(Prelude Axioms) extructures(ord fset fmap) Mon(SPropBase) Equations(Equations)