agdaじゃなくてcoqになっちゃうけど http://proofcafe.org/sf/ を手を動かしながらやると実感できるよ
↑は日本語だからとっつきやすいし、大体がagdaに適用できるはず。Prop_Jまで読んで触れば分かるはず