>>200
証明論における代入について詳しく