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

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