In http://www.ens-lyon.fr/~plescann/PUBLICATIONS/RecursiveTypes/ I put
a copy of a paper by Claude Pair published in Algol Bulletin n. 31,
March 1970, which provides a first proof of the decision of equality
in recursive types.
As this paper is not easily available, I thought that that the types
community could be interested.
Best regards,
Pierre Lescanne