Theorem: convIf.id (One.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