no goals
α : Type ?u.44
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Pow M ℕ
P : Prop
inst✝ : Decidable P
a : M
b c : ℕ
⊢ (a ^ if P then b else c) = if P then a ^ b else a ^ c
split_ifs <;> rfl