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