Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/setConfig
/
.
/
tests
/
lean
/
arrayGetU.lean.expected.out
blob: e47fb37ac3a4716ab4c3abdc476d74b9f1e05b4b [
file
] [
edit
]
i j
:
Nat
a
:
Array
Nat
v
:
Nat
h
₁
:
i
<
a
.
size
h
₂
:
j
<
a
.
size
h
₃
:
i
=
j
⊢
f a i v h
₁
=
f a j v h
₂
i j
:
Nat
a
:
Array
Nat
v
:
Nat
h
₁
:
0
+
i
<
a
.
size
h
₂
:
j
<
a
.
size
h
₃
:
i
=
j
⊢
f a i v
(
Nat
.
zero_add i
▸
h
₁)
=
f a j v h
₂