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