Kleene Sections ClassicalProps(jlc) Doc

Def 3 == inr(inr())

is mentioned by

Thm* x,y:. x y = 3 x = 3 y = 3[K_or_equal_Three_2]
Thm* x,y:. x y = 3 x = 3 & y = 3[K_and_equal_Three_2]
Def p q == case p: 3 q; 3 case q: 3 3; 3 3; 3 3;; 3 3;[K_or]
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]

In prior sections: Three

Try larger context: ClassicalProps(jlc)

Kleene Sections ClassicalProps(jlc) Doc