DISP	three_df	3== 3
ABS	three	3 == 3
THM	three_wf	3
DISP	Three_df	==
ABS	Three	== Unit + ?Unit
THM	Three_wf
DISP	Three_0_df	3== 3
ABS	Three_0	3 == inl
THM	Three_0_wf	3
DISP	Three_1_df	3== 3
ABS	Three_1	3 == inr (inl )
THM	Three_1_wf	3
DISP	Three_2_df	3== 3
ABS	Three_2	3 == inr inr
THM	Three_2_wf	3
DISP	Three_case_df	case{->0} <T:Three:L>: 3 <case0:3 case:L> 3 <case1:3 case:L> ; 3 <case2:3 case:L> == case <T>: 3 <case0> 3 <case1> 3 <case2>
ABS	Three_case	case x: 3 case0; 3 case1; 3 case2; == case x of inl(zero) => case0 | inr(one_or_two) => case one_or_two of inl(one) => case1 | inr(two) => case2
ML	Three_case_unroll	let get_three_case_arg = fst o fst o dest_term o snd o hd o snd o dest_term;; let three_caseC t = let arg = (get_three_case_arg t) in (FwdMacroC (concat `Three_case_` (concat arg `_unrollC`)) (AllC [UnfoldC `Three_case`; UnfoldC arg; ReduceC]) t) ;; let Three_case_unrollC = FirstC[three_caseC case 3: 3 case0; 3 case1; 3 case2;; three_caseC case 3: 3 case0; 3 case1; 3 case2;; three_caseC case 3: 3 case0; 3 case1; 3 case2;] ;; add_AbReduce_conv `Three_case` Three_case_unrollC;;
ML	ThreeCase	let ThreeCases i p = (let i = get_pos_hyp_num i p in let f = (\n. D i THEN Fold `it` 0 THEN Fold n 0 THEN UnivCD THENA Auto) in MoveDepHypsToConclFor (\i. D (i) THENL [f `Three_0`; D (i) THENL [f `Three_1`; f `Three_2`]]) i THENA Auto ) p ;;
ML	Three_ind	let ThreeInd i p = (let j = get_pos_hyp_num i p in let AllFolds l = (Repeat (TryOnAllHyps (\i. Folds l i) THEN Try (Folds l 0))) in Unfold `Three` j THEN D j THENL [Id; D j] THEN UnitInd j THENL [ AllFolds ``Three_0``; AllFolds ``Three_1``; AllFolds ``Three_2``] ) p ;;
THM	Three_ind_ext	x:. True
ML	Three_eq_contradiciton	let mk_Three_case v = mk_simple_term `Three_case` [mvt v; 0; 1; 2] ;; let ThreeNEQ i p = let j = get_pos_hyp_num i p in let v = maybe_new_var `x' (declared_vars p) in (ApFunToHypEquands v (mk_Three_case v) j THENA Auto THENL [ThreeInd (-1) THEN AbReduce 0 THEN Auto; AbReduce (-1) THEN Auto]) p ;;
THM	Three_eq_contradiction_ext	(3 = 3)
THM	Three_case_wf_0	t:. t':{j}. t'':{k}. c:t. c':t'. c'':t''. case 3: 3 c; 3 c'; 3 c''; t
THM	Three_case_wf_1	t:. t':{j}. t'':{k}. c:t. c':t'. c'':t''. case 3: 3 c'; 3 c''; 3 c; t''
THM	Three_case_wf_2	t:. t':{j}. t'':{k}. c:t. c':t'. c'':t''. case 3: 3 c; 3 c'; 3 c''; t''
THM	decidable__equal_Three	x,y:. Dec(x = y)

the other theories