chore: fix test
This commit is contained in:
parent
d3bc963e92
commit
ec932e389b
1 changed files with 1 additions and 1 deletions
|
|
@ -4,7 +4,7 @@ as bs : List α
|
|||
h : bs = a :: as
|
||||
⊢ List.length (?a_1 :: as) = List.length bs
|
||||
|
||||
case a_1
|
||||
case a
|
||||
α : Type ?u
|
||||
a : α
|
||||
as bs : List α
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue