no goals
α : Type u_1
β : Type u_2
γ : Type ?u.30447
δ : Type ?u.30450
ε : Type ?u.30453
ι : Type ?u.30456
f : α →. β ⊕ α
b : β
a a' : α
hb : b ∈ fix f a
ha' : Sum.inr a' ∈ f a
⊢ b ∈ fix f a'
rwa [← fix_fwd_eq ha']