more on readme

Author: Andrei Popescu

README.md

@@ -145,31 +145,44 @@ As discussed in Sect. 9 and App. G, we have automated the production of binding-
 
 #### For the main paper 
 
-
-##### Appendix A
+##### Section 2
 
 Prop 1 --> subsumed by Prop. 2 (also generated and proved automatically by the standard inductive definition)
 
 Prop 2 --> theorem `step.strong_induct` (generated and proved by `binder_inductive`) from thys/Untyped_Lambda_Calculus
 
+##### Sections 3 and 4
+
 Thms 4 and 5 --> just recallections of the standard result (available in the Isabelle library)
 
 Thm 7 (already the strengthened version discussed in Sect. 7.3) --> theorem `strong_induct_nom` (in locale `Induct_nom`) from thys/Generic_Strong_Rule_Induction.thy.
 
+##### Section 7.1
+
 Prop 12 --> theorems called `trans.strong_induct` (generated and proved by `binder_inductive`) from Pi_Transition_Early.thy and Pi_Transition_Late.thy. (As explained in the paper, Prop 12 actually shows a hybrid containing a selection of the more interesting rules for the two types of transitions.)
 
+##### Section 7.2
+
 Prop 13 --> theorem `ty.strong_induct` (generated and proved by `binder_inductive`) from thys/POPLmark/SystemFSub.thy
 
+##### Section 8.1
+
 Prop 15 --> theorem `deduct.strong_induct` (generated and proved by `binder_inductive`) from thys/Infinitary_FOL/InfFOL.thy
 
+##### Section 8.2
+
 Counterexample 16 --> theorem `counterexample` from No_Least_Support_Counterexample.thy
 
 Thm 19 --> theorem `strong_induct` (in locale `Induct`) from thys/Generic_Strong_Rule_Induction.thy.
 
+##### Section 8.3
+
 Prop 20 --> theorem `affine.strong_induct` (generated and proved by `binder_inductive`) from thys/Infinary_Lambda_Calculus/ILC_affine.thy
 
 Prop 21 --> theorem `strong_induct_reneqv` from ILC_Renaming_Equivalence.thy
 
+##### Section 8.4
+
 Thm 22 --> theorem `strong_iinduct` (in locale `IInduct`) from thys/Generic_Strong_Rule_Induction.thy.