DISP	K_imp_df	<p::*> <q::*>== <p> <q>
ABS	K_imp	p q == case p: 3 3; 3 case q: 3 3; 3 3; 3 3;; 3 q;
THM	K_imp_wf	p,q:. p q
DISP	K_not_df	<p::*>== <p>
ABS	K_not	p == case p: 3 3; 3 3; 3 3;
THM	K_not_wf	p:. p
DISP	K_and_df	<p::*> <q::*>== <p> <q>
ABS	K_and	p q == case p: 3 3; 3 case q: 3 3; 3 3; 3 3;; 3 q;
THM	K_and_wf	p,q:. p q
DISP	K_or_df	<p::*> <q::*>== <p> <q>
ABS	K_or	p q == case p: 3 q; 3 case q: 3 3; 3 3; 3 3;; 3 3;
THM	K_or_wf	p,q:. p q
ML	Kleene_op_unroll	let K_opC t = let op = fst (fst (dest_term t)) in (FwdMacroC (concat op `_unrollC`) (AllC [UnfoldC op; Three_case_unrollC]) t ) ;; let K_not_unrollC = FirstC [K_opC 3; K_opC 3; K_opC 3] ;; add_AbReduce_conv `K_not` K_not_unrollC;; let K_and_unrollC = FirstC [K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3] ;; add_AbReduce_conv `K_and` K_and_unrollC;; let K_or_unrollC = FirstC [K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3] ;; add_AbReduce_conv `K_or` K_or_unrollC;; let K_imp_unrollC = FirstC [K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3; K_opC 3 3] ;; add_AbReduce_conv `K_imp` K_imp_unrollC;;
THM	K_and_equal_Three_2	x,y:. x y = 3 x = 3 y = 3
THM	K_or_equal_Three_2	x,y:. x y = 3 x = 3 y = 3

the other theories