Kleene Sections ClassicalProps(jlc) Doc

Def p q == case p: 3 q; 3 case q: 3 3; 3 3; 3 3;; 3 3;

is mentioned by

Thm* x,y:. x y = 3 x = 3 y = 3[K_or_equal_Three_2]

Try larger context: ClassicalProps(jlc)

Kleene Sections ClassicalProps(jlc) Doc