DISP	Sequent_df	Sequent== Sequent
ABS	Sequent	Sequent == Formula List Formula List
THM	Sequent_wf	Sequent
THM	product_inc_Sequent	Formula List Formula List Sequent
THM	pair_wf_Sequent	h,c:Formula List. <h, c> Sequent
THM	Sequent_inc	Sequent Formula List Formula List
DISP	H_df	<s:Sequent:L>.H== <s>.H
ABS	H	s.H == let <h,c> = s in h
THM	H_wf	s:Sequent. s.H Formula List
DISP	C_df	<s:Sequent:L>.C== <s>.C
ABS	C	s.C == let <h,c> = s in c
THM	C_wf	s:Sequent. s.C Formula List
ML	HC_unroll	let H_unrollC = FwdMacroC `H_unrollC` (UnfoldC `H` ANDTHENC ReduceC ) <h, c>.H ;; let C_unrollC = FwdMacroC `C_unrollC` (UnfoldC `C` ANDTHENC ReduceC ) <h, c>.C ;; let HC_unrollC = C_unrollC ORELSEC H_unrollC;; add_AbReduce_conv `H` H_unrollC;; add_AbReduce_conv `C` C_unrollC;;

the other theories