DISP	mono_df	Mono{ < i:level > }( < b:b-var > , < x:x-var > . < B:B:* > on < T:T:* > ) == Mono{ < i > }( < b > , < x > . < B > on < T > )
ABS	mono	Mono{i}(b,x.B[b; x] on T) == b',b'':T . (x:T. b' x b'' x) (x:T. B[b'; x] B[b''; x])
THM	mono_wf	T:. B:(T ) T . Mono{i}(b,x.B[b;x] on T) '
DISP	parec_df	parec( < A:A-var > , < x:x-var > . < B:B:* > @ < a:a:* > ) == parec( < A > , < x > . < B > @ < a > )
ABS	parec	parec(A,x.B[A; x] @ a) == !null_abstraction
DISP	parec_ind_df	parec_ind( < r:r:* > ; < h:var > , < z:var > . < t:t:* > ) == parec_ind( < r > ; < h > , < z > . < t > )
ABS	parec_ind	parec_ind(r;h,z.t[h; z]) == !null_abstraction
RULE	parecEquality	H parec(b1,x1.B1 @ t1) = parec(b2,x2.B2 @ t2) BY parecEquality x T b H t1 = t2 H, x:T, b:(T ) B1[b,x/b1,x1] = B2[b,x/b2,x2] H Mono{i}(b1,x1.B1 on T)
THM	parec_wf	T:. B:(T ) T . t:T. Mono{i}(b,x.B[b;x] on T) parec(b,x.B[b;x] @ t)
RULE	parecMemberEquality	H b1 = b2 BY parecMemberEquality level{i} z H b1 = b2 H parec(b,x.B @ t) = parec(b,x.B @ t)
ML	parecEqTypeCD_tac	let ParecEqTypeCD p = let T, (), () = dest_equal (concl p) in (Refine `parecMemberEquality` (infer_level_exp_arg p T . mk_new_var_args [[get_optional_var_arg `v1` p; mkv `z`]] p ) THENL [Id;WFPrettyUp] ) p ;; let ParecMemTypeCD = UnfoldTop `member` 0 THEN ParecEqTypeCD THENL [FoldTop `member` 0;Id] ;; let AbParecMemTypeCD p = let T, () = dest_member (concl p) in let parecid =opid_of_term T in (Unfold parecid 0 THEN ParecMemTypeCD THEN (Fold parecid 0) THEN Reduce 0 ) p ;;
RULE	parecUnroll	H, r:parec(b,x.B @ t), J G ext g[r/r'] BY parecUnroll #$i r' z u H, r:parec(b,x.B @ t), J, r':B[(z.parec(b,x.B @ z)),t/b,x], u:(r = r') G[r'/r] ext g
ML	parecTypeHD_tac	let ParecTypeHD i p = let i' = get_pos_hyp_num i p in let v, T = dest_hyp i' p in if not is_term `parec` T then failwith `ParecTypeHD : not parec type` else Refine `parecUnroll` (mk_int_arg i' . mk_new_var_args [[get_optional_var_arg `v1` p; v]; [get_optional_var_arg `v2` p; mkv `z`]; [] ] p ) p ;; let AbParecTypeHD i p = let i' = get_pos_hyp_num i p in let v, T = dest_hyp i' p in let parecid = opid_of_term T in (Unfold parecid i' THEN ParecTypeHD i' THEN Fold parecid i' THEN Reduce (-2) THEN Fold parecid (-2) ) p ;;
RULE	parecMemberFormation	H parec(b,x.B @ a) ext t BY parecMemberFormation level{i} z H B[(z.parec(b,x.B @ z)),a/b,x] ext t H parec(b,x.B @ a)
RULE	parecElimination	H, t:T, J, r:parec(b,x.B @ t), J1 G ext parec_ind(t;w,z.g[(t,r.Void)/u]) BY parecElimination level{i} #$j1 #$j2 u w v s z H, t:T, J, r:parec(b,x.B @ t), J1 parec(b,x.B @ t) = parec(b,x.B @ t) H, t:T, J, r:parec(b,x.B @ t), J1, u:(t:T parec(b,x.B @ t) ) w:(t:T r:{v:parec(b,x.B @ t)| u t v} G), s:T z:B[(s.{v:parec(b,x.B @ s)| u s v} ),s/b,x] G[s,z/t,r] ext g
ML	parecInd_tac	let ParecInd i j p = let i' = get_pos_hyp_num i p in let j' = get_pos_hyp_num j p in let t, T = dest_hyp i' p in let r, P = dest_hyp j' p in (Refine `parecElimination` (infer_level_exp_arg p T . mk_int_arg i' . mk_int_arg j' . mk_new_var_args [[get_optional_var_arg `v1` p; mkv `Q`]; []; [get_optional_var_arg `v3` p; mkv `v`]; [get_optional_var_arg `v4` p; t]; [get_optional_var_arg `v5` p; r] ] p ) THENL [WFPrettyUp; FoldAtAddr `prop` [2;2] (-4) THEN FoldTop `all` (-3) THEN FoldAtAddr `all` [2] (-3)] ) p ;; let AbParecInd i j p = let i' = get_pos_hyp_num i p in let j' = get_pos_hyp_num j p in let r, P = dest_hyp j' p in let parecid = opid_of_term P in (Unfold parecid j' THEN ParecInd i' j' THEN Fold parecid j' THENL [ Fold parecid 0 ; Fold parecid (-1) THEN Fold parecid (-3) THEN Fold parecid (-4)] ) p ;;
RULE	parec_indEquality	H parec_ind(r1;h1,z1.t1) = parec_ind(r2;h2,z2.t2) BY parec_indEquality level{i} (x.S[x/r1]) (a:A parec(A,x.B @ a)) Z u h z H r1 = r2 H, Z:(A ), u:(z:(a:A Z a) (z = z)), h:(z:(a:A Z a) S[z/x]), z:(a:A B[Z/A][a/x]) t1[h/h1][z/z1] = t2[h/h2][z/z2]

the other theories