Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/expose-array-back
/
.
/
tests
/
elab
/
matchVarIssue.lean
blob: 5d5a2b6656b64c93f4b3211ec3249e99f4250b75 [
file
] [
edit
]
theorem ex
{
c d
:
Char
}
:
c
=
d
→
c
.
val
=
d
.
val
|
rfl
=>
rfl
