summaryrefslogtreecommitdiff
path: root/Common/Function.lean
blob: 691a0686bd2db4abfcb35e1b548f7ebbb9e38b52 (plain) (blame)
1
theorem Function.comp_assoc (f : γ  δ) (g : β  γ) (h : α  β) : (fg)h = fgh := rfl