Add formal semantic of Alethe

- Define what a valid Alethe proof is formally
- Show that a valid Alethe proof is sound
- TODO: nicer handling of let

spec/rule_list.tex

@@ -1528,7 +1528,9 @@ The possible transformations are:
   \end{plContainer}
   where $\simeq$ is replaced by $\leftrightarrow$ where necessary.
 
-  If for $t_i\simeq s_i$ the $t_i$ and $s_i$ are syntactically equal, the premise
+	The premise $i_1, \dots, i_n$ must be in the same subproof as
+	the $currule$ step.  If for $t_i\simeq s_i$ the $t_i$ and $s_i$
+	are syntactically equal, the premise
   is skipped.
 
 \end{proof-rule}