S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x✝ : Option Γ'
⊢ Λ'.Supports S (ite (x✝ = some Γ'.consₗ) id (Λ'.clear (fun x => decide (x = Γ'.consₗ)) k) (unrev q))
S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x✝ : Option Γ'
⊢ Λ'.Supports S ((fun s => ite (s = some Γ'.consₗ) id (Λ'.clear (fun x => decide (x = Γ'.consₗ)) k) (unrev q)) x✝)
dsimp only
no goals
S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x✝ : Option Γ'
⊢ Λ'.Supports S (ite (x✝ = some Γ'.consₗ) id (Λ'.clear (fun x => decide (x = Γ'.consₗ)) k) (unrev q))
split_ifs <;> exact H