conv at h => ext; ext; ext; rw [← List.foldr_reverse]
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ x ∈ fold c insert empty ↔ x ∈ c
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L.reverse
⊢ x ∈ fold c insert empty ↔ x ∈ c