§ Using reduceBool and ofReduceBool in Lean

import Lean
open Lean

abbrev foo.aux : Bool := decide (true = true)

#check @of_decide_eq_true

theorem foo : true = true := @of_decide_eq_true (p := true = true) (inst := inferInstance) 
  (@Lean.ofReduceBool foo.aux _ (by rfl))

-- tactic 'rfl' failed ...
theorem foo' : true = true := @of_decide_eq_true (p := true = true) (inst := inferInstance) 
  (@Lean.ofReduceBool _ _ (by rfl))