(3steps)
PrintForm
Definitions
Kleene
Sections
ClassicalProps(jlc)
Doc
At:
K
or
wf
1
1.
p:
2.
q:
p
q
By:
Unfold `K_or` 0
Generated subgoal:
1
case p: 3
q; 3
case q: 3
3
; 3
3
; 3
3
;; 3
3
;
About:
(3steps)
PrintForm
Definitions
Kleene
Sections
ClassicalProps(jlc)
Doc