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