Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/replace
/
.
/
tests
/
lean
/
1682.lean.expected.out
blob: cd49d31eeb7a4a297de7d0409bf35de773208bcd [
file
] [
edit
]
1682.lean
:
1
:
25
-
2
:
17
:
error
:
unsolved goals
case
a
p
:
Sort
?
u
q r
:
Prop
⊢
p
→
q
case
b
p
:
Sort
?
u
q r
:
Prop
⊢
r
1682.lean
:
4
:
25
-
5
:
26
:
error
:
unsolved goals
case
a
p
:
Sort
?
u
q r
:
Prop
h
:
p
⊢
q
case
b
p
:
Sort
?
u
q r
:
Prop
⊢
r