Kleene Sections ClassicalProps(jlc) Doc

Def case x: 3 case0; 3 case1; 3 case2; == InjCase(x; zero. case0; one_or_two. InjCase(one_or_two; one. case1; two. case2))

is mentioned by

Def p q == case p: 3 q; 3 case q: 3 3; 3 3; 3 3;; 3 3;[K_or]
Def p q == case p: 3 3; 3 case q: 3 3; 3 3; 3 3;; 3 q;[K_and]
Def p == case p: 3 3; 3 3; 3 3;[K_not]
Def p q == case p: 3 3; 3 case q: 3 3; 3 3; 3 3;; 3 q;[K_imp]

Try larger context: ClassicalProps(jlc)

Kleene Sections ClassicalProps(jlc) Doc