Theorem: SciLean.ConvIf.convIf.id (SciLean/Tactic/ConvIf.lean)

State before:
α : Sort u_1
P : Prop
inst : Decidable P
a : α
⊢ a = convIf P inst (fun x => a) fun x => a
Tactic:
simp[convIf]
State after:
no goals