We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 1c06e62 commit 8e37a9bCopy full SHA for 8e37a9b
AesopTest/27.lean
@@ -24,7 +24,7 @@ trace: [aesop.proof] Final proof:
24
((fun (h_2 : All P (x :: xs)) =>
25
(casesOn (P := P) (motive := fun a x_1 => x :: xs = a → h ≍ x_1 → P x ∧ All P xs) h_2
26
(fun h_3 => False.elim (noConfusion_of_Nat List.ctorIdx h_3)) fun {x_1} {xs_1} a a_1 h_3 =>
27
- List.cons.noConfusion (h ≍ cons (P := P) a a_1 → P x ∧ All P xs) x xs x_1 xs_1 h_3 fun head_eq =>
+ List.cons.noConfusion h_3 fun head_eq =>
28
Eq.ndrec (motive := fun {x_1} =>
29
∀ (a : P x_1), xs = xs_1 → h ≍ cons (P := P) a a_1 → P x ∧ All P xs)
30
(fun a tail_eq =>
0 commit comments