Commit 2021-11-01 08:32 999cd055
View on Github →refactor(remove Decidable.to_bool) (#82)
Decidable.to_bool seems to be in the prelude as Decidable.decide; the removed lemmas to_bool_true_eq_tt and to_bool_false_eq_ff correspond to the prelude's decide_true_eq_true and decide_false_eq_false.