(3steps)
PrintForm
Definitions
Kleene
Sections
ClassicalProps(jlc)
Doc
At:
K
imp
wf
1
1
1.
p:
2.
q:
case p: 3
3
; 3
case q: 3
3
; 3
3
; 3
3
;; 3
q;
By:
Repeat (ThreeInd 1 THEN AbReduce 0)
Generated subgoals:
None
About:
(3steps)
PrintForm
Definitions
Kleene
Sections
ClassicalProps(jlc)
Doc