+a : applicability condition (true = restricted, false = general)
+b : local dropping kind parameter (true = restricted, false = general)
+c : rt-reduction count parameter
+d : term degree
+e : reserved: future use (\lambda\delta 3)
+f,g : local reference transforming map