Fix theorem reference in README

Author: jvanbruegge

README.md

@@ -48,7 +48,7 @@ The formalization is organized into the following sessions:
 | -------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
 | Isabelle_Prelim            | Administrative session bundling the standard Isabelle libraries that we use.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
 | Prelim                     | Miscellaneous extensions to standard libraries, and bindings-specific infrastructure (e.g., countable and uncountable types we use for variables).                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |
-| Binders                    | Main metatheory including the formalization our Thms 19, called strong_induct in the formalization, and 22 (called BE_iinduct in Generic_Strong_Rule_Induction.thy (Sect. 4, 8.3, 9.2, 9.4 and App. G.2), the proof that our results generalize the Urban/Berghofer/Norrish criterion in Urban_Berghofer_Norrish_Rule_Induction.thy (claimed in the paper and detailed in App. A), and the binding-aware datatype automation in MRBNF_Composition.thy and MRBNF_Recursor.thy and various ML files (App. G). Also contains the formalization of Counterexample 16 (Sect. 9.2) in No_Least_Support_Counterexample.thy. |
+| Binders                    | Main metatheory including the formalization our Thms 19, called strong_induct in the formalization, and 22 (called strong_iinduct in Generic_Strong_Rule_Induction.thy (Sect. 4, 8.3, 9.2, 9.4 and App. G.2), the proof that our results generalize the Urban/Berghofer/Norrish criterion in Urban_Berghofer_Norrish_Rule_Induction.thy (claimed in the paper and detailed in App. A), and the binding-aware datatype automation in MRBNF_Composition.thy and MRBNF_Recursor.thy and various ML files (App. G). Also contains the formalization of Counterexample 16 (Sect. 9.2) in No_Least_Support_Counterexample.thy. |
 | Untyped_Lambda_Calculus    | Formalization of the untyped lambda calculus including beta reduction and parallel beta reduction (Sect. 2).                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
 | Process_Calculus           | Formalization of the pi-calculus transition relation and the associated strong rule induction principle (Sect. 8.1 and App. D.3) -- covering both the early-instantiation and late-instantiation semantics, in theories Pi_Transition_Early.thy and Pi_Transition_Late.thy                                                                                                                                                                                                                                                                                                                                           |
 | System_Fsub                | Formalization of System F with subtyping, the associated strong rule induction principles, and the POPLmark challenge 1A (Sect. 8.2 and App. F).                                                                                                                                                                                                                                                                                                                                                                                                                                                                     |