proposition: Theorem equiv_dec_refl_left : forall a, @EquivDec.equiv_dec _ _ _ dec a a = left eq_refl.
proof: Proof. intros. destruct (EquivDec.equiv_dec a a); try congruence. f_equal. apply UIP_equal. Qed.
imports: ExtLib.Core.RelDec ExtLib.Tactics.Consider