fe3c7394fd
This PR fixes the invariant in `grind` AC. equations in the todo queue are not fully simplified.
7 lines
160 B
Text
7 lines
160 B
Text
public section
|
||
|
||
namespace List
|
||
|
||
set_option grind.debug true in
|
||
theorem take_eq_self_iff (x : List α) {n : Nat} : x.take n = x → x.length ≤ n := by
|
||
grind
|