Proof Method. `erule` [isa-0011]

November 28, 2025
Liam O'Connor

Given a goal $\llbracket X; A_1 \dots A_n \rrbracket \implies G$ and a theorem r $: \llbracket X; P_1 \dots P_n \rrbracket \implies G$ (typically an elimination rule where the conclusion is just a variable, easily unified with $G$ ), apply (erule r) replaces the goal with subgoals:

$\llbracket A_1 \dots A_n \rrbracket \implies P_1$
$\dots$
$\llbracket A_1 \dots A_n \rrbracket \implies P_n$