fact: Parameter choose_equal : forall s s', Equal s s' -> match choose s, choose s' with | inleft (exist _ x _), inleft (exist _ x' _) => E.eq x x' | inright _, inright _ => True | _, _ => False end.
imports: Bool OrderedType DecidableType