Description: Obsolete version of isarep1 as of 19-Dec-2024. (Contributed by NM, 26-Oct-2006) (Proof shortened by Mario Carneiro, 4-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)