Kleene Sections ClassicalProps(jlc) Doc

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

is mentioned by

Thm* x,y:. x y = 3 x = 3 & y = 3[K_and_equal_Three_2]

Try larger context: ClassicalProps(jlc)

Kleene Sections ClassicalProps(jlc) Doc