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