liamoc.net
my forest
1\date{2025-11-28T05:41:54Z}
2\taxon{Proof Method}
3\title{\code{rule}}
4\author{liamoc}
5\p{Given a goal #{\llbracket A_1 \dots A_n \rrbracket \implies G} and a theorem \code{r}#{: \llbracket P_1 \dots P_n \rrbracket \implies G} (commonly an introduction rule),
6\code{apply (rule r)} replaces the goal with subgoals:
7\ul{\li{#{\llbracket A_1 \dots A_n \rrbracket \implies P_1 }}\li{ #{\dots}}\li{ #{\llbracket A_1 \dots A_n \rrbracket \implies P_n }}}
8}
9\scope{
10\put\transclude/toc{false}
11\subtree{
12 \taxon{Aside}
13 \p{Technically, the conclusion of the rule and the goal do not have to be exactly equal, but they must be \em{unifiable} – that is, there must be some substitution to schematic variables that makes the conclusion of the rule and the goal equal.}
14}}