DISP	curry_df	curry <f:Function:L>== curry <f>
ABS	curry	curry f == x,y.f <x, y>
THM	curry_wf	T:. U:{j}. V:{k}. f:(T U) V. curry f T U V
DISP	uncurry_df	uncurry <f:function:L>== uncurry <f>
ABS	uncurry	uncurry f == x.let <l,r> = x in f l r
THM	uncurry_wf	T:. U:{j}. V:{k}. f:T U V. uncurry f (T U) V
THM	curry_uncurry_inverse	T:. U:{j}. V:{k}. f:(T U) V. f = uncurry curry f
THM	uncurry_curry_inverse	T:. U:{j}. V:{k}. f:T U V. f = curry uncurry f
DISP	letrec_df	(letrec <f:Name> <b:Args & Body:L>) == (letrec <f> <b>)
ABS	letrec	(letrec f b[f]) == Y (f.b[f])
DISP	letrec_body_df	= <b:Body:L> == = <b>
ABS	letrec_body	= b == b
DISP	letrec_arg_df	<x:Arg> <b:Args & Body:L> == <x> <b>
ABS	letrec_arg	x b[x] == x.b[x]
ML	letrec_unroll	let letrec_unrollTopC = FwdMacroC `letrec_unrollTopC` (UnfoldC `letrec` ANDTHENC HigherC YUnrollC ANDTHENC ReduceC ANDTHENC FoldC `letrec`) (letrec f b[f]) ;; letrec letrec_unrollArgsC e = (IfC (\e. is_apply_term) (NthSubC 1 letrec_unrollArgsC ANDTHENC RedexC) ORELSEC IfC (\e t. (is_term `letrec_arg` t)) (NthSubC 1 letrec_unrollArgsC ANDTHENC UnfoldTopAbC) ORELSEC IfC (\e t. (is_term `letrec_body` t)) UnfoldTopAbC ) e ;; let letrec_unrollC = HigherC letrec_unrollTopC ANDTHENC letrec_unrollArgsC ;;
ML	letrec_tac	let LetrecMemberCD (name: token) = Unfold name 0 THEN Rewrite (HigherC letrec_unrollC) 0 THEN Auto ;;
DISP	theta_df	T== T
ABS	theta	T == (x,y.y (x x y)) (x,y.y (x x y))
ML	theta_unroll	let theta_unrollC = FwdMacroC `theta_unrollC` (AllC [UnfoldC `theta`; HigherC RedexC; FoldC `theta`; NthC 1 RedexC; NthC 1 RedexC]) T (f.N[f]) ;;
DISP	applicative_Y_df	Y== Y
ABS	applicative_Y	Y == f.(x.f (y.x x y)) (x.f (y.x x y))
ML	applicative_Y_unroll	let applicative_Y_unrollC = FwdMacroC `applicative_Y_unrollC` (AllC [UnfoldC `applicative_Y`; (SweepUpC RedexC) ]) Y (f.N[f]) ;;

the other theories