(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:
member

(3steps) PrintForm Definitions Kleene Sections ClassicalProps(jlc) Doc