+-- A1. No top-level variable is bound in the target
+-- A2. No template variable is bound in the target
+-- A3. No lambda bound template variable is free in any subexpression of the target
+--
+-- To see why A1 is necessary, consider matching
+-- \x->f against \f->f
+-- When we meet the lambdas we substitute [f/x] in the template (a no-op),
+-- and then erroneously succeed in matching f against f.
+--
+-- To see why A2 is needed consider matching
+-- forall a. \b->b against \a->3
+-- When we meet the lambdas we substitute [a/b] in the template, and then
+-- erroneously succeed in matching what looks like the template variable 'a' against 3.
+--
+-- A3 is needed to validate the rule that says
+-- (\x->E) matches F
+-- if
+-- (\x->E) matches (\x->F x)
+