ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
l : List ι
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
⊢ ∀ (a : α) (b : β), f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
l : List ι
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
a : α
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
⊢ f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l
revert a b
no goals
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
l : List ι
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
⊢ ∀ (a : α) (b : β), f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l
induction l <;> intros <;> [rfl; simp only [*, foldl]]