module finite_rel.

kind finite_rel		type -> type -> type.

type empty_f_rel 	(finite_rel Domain Range).
type f_rel_extend	Domain -> Range -> (finite_rel Domain Range)
				-> (finite_rel Domain Range).
type f_rel_apply	(finite_rel Domain Range) -> Domain -> Range -> o.
type f_rel_in_domain	(finite_rel Domain Range) -> Domain -> o.


f_rel_apply (f_rel_extend DomainElem Res FF) DomainElem Res :- !.
f_rel_apply (f_rel_extend DomainElem Res FF) X Y :-
	f_rel_apply FF X Y.

f_rel_in_domain (f_rel_extend DomainElem Res FF) DomainElem :- !.
f_rel_in_domain (f_rel_extend DomainElem Res FF) X :-
	f_rel_in_domain FF X.