Empty list is left identity for append
Closed
Theorem & proof
·
list_nil_append.lean
·
✓ verified
1
2
3
import Mathlib theorem list_nil_append {α : Type} (l : List α) : [] ++ l = l := rfl
Rewards pledged
No rewards pledged yet.