DISP	discrete_df	Discrete{<T:type:L>}== Discrete{<T>}
ABS	discrete	Discrete{T} == x,y:T. Dec(x = y)
THM	discrete_wf	T:. Discrete{T} '
THM	discrete_implies_bool_equality	T:. Discrete{T} (f:T T . x,y:T. (f x y) x = y)
DISP	discrete_equality_df	{<T:type:L>=}== {<T>=}
ABS	discrete_equality	{T=} == {eq:T T | x,y:T. (eq x y) x = y}
THM	discrete_equality_wf	T:. {T=}
THM	discrete_equality_inc	T:. {T=} T T
THM	discrete_equality_properties	T:. eq:{T=}. (x,y:T. (eq x y) x = y) eq T T
ML	discrete_eq_tac	let is_discrete_equality_term t = (opid_of_term t) = `discrete_equality` ;; let is_discrete_term t = (opid_of_term t) = `discrete` ;; let DiscreteEq i p = (let T = type_of_hyp i p in let i = get_pos_hyp_num i p in if is_discrete_equality_term T then let name = mk_var_term (var_of_hyp i p) in let type = hd (subterms_of_term T) in InstLemma `discrete_equality_properties` [type;name] THENA Auto THEN D (-1) THEN CopyToHyp (i + 1) (-2) THEN Thin (-2) THEN CopyToHyp (i + 1) (-1) THEN Thin (-1) else failwith `DiscreteEq: hyp is not an discrete_equality term.` )p ;; let MkDiscreteEqInst i p = (let T = type_of_hyp i p in let i = get_pos_hyp_num i p in let dvars = (declared_vars p) in let eq = maybe_new_var (mkv `eq`) dvars in if is_discrete_term T then FwdThruLemma `discrete_implies_discrete_equality` [i] THENA Auto THEN D (-1) THEN Thin (-1) THEN CopyToHyp (i + 1) (-1) THEN Thin (-1) THEN RenameVar eq (i + 1) THEN DiscreteEq (i + 1) else failwith `MkDiscreteEq: hyp is not a discrete term.` )p ;; let MkDiscreteEq t = InstLemma (concat `discrete__` t) [] THENA Auto THEN MkDiscreteEqInst (-1) THEN OnHyps [-4;-2;-1] Thin ;; let MkDiscreteEqWith t name i = MkDiscreteEq t THEN MoveToHyp i (-1) THEN RenameVar name i ;;
THM	discrete_implies_discrete_equality	T:. Discrete{T} (f:{T=}. True)
THM	discrete_equality_unique	T:. f1,f2:{T=}. f1 = f2
THM	discrete_equality_reflexive	T:. eq:{T=}. u:T. (eq u u)
THM	discrete_equality_symmetric	T:. eq:{T=}. x,y:T. (eq x y) (eq y x)
THM	discrete_equality_transitive	T:. eq:{T=}. x,y,z:T. (eq x y) (eq y z) (eq x z)
THM	discrete__union	T1:. T2:{j}. Discrete{T1} Discrete{T2} Discrete{(T1 + T2)}
THM	discrete__product	T1:. T2:{j}. Discrete{T1} Discrete{T2} Discrete{(T1 T2)}
THM	discrete__atom	Discrete{Atom}

the other theories