またもアドバイスいただきました (rev2 (rev2 l nil) nil) = l なら (rev2 (rev2 l (cons a nil)) nil) = (cons a l)ですね。この証明にも、rev2の引数がrcons（またはappend）である場合の補題が必要になるとおもいます。— SUHARA Hiromichi (@suharahiromi…