import Leanopen Leanabbrev foo.aux : Bool := decide (true = true)#check @of_decide_eq_truetheorem 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))