module fndef.


copy X X :- const X.
copy (A @ B) (C @ D) :- copy A C, copy B D.
copy (abs Ps Ty L) (abs Ps Ty M) :- pi x\ (copy x x => (copy (L x) (M x))).
copy (freevar S) (freevar S).   % will be superceded by !
copy (tm_coerce A) (tm_coerce A).