Proof Method. rule [isa-000Z]

Given a goal \llbracket A_1 \dots A_n \rrbracket \implies G and a theorem r: \llbracket P_1 \dots P_n \rrbracket \implies G (commonly an introduction rule), apply (rule 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

Aside.

Technically, the conclusion of the rule and the goal do not have to be exactly equal, but they must be unifiable – that is, there must be some substitution to schematic variables that makes the conclusion of the rule and the goal equal.