stating the strong induction; further.
quick_and_dirty := true;
no_document use_thys
["Nominal2_Base",
"Nominal2_Eqvt",
"Nominal2_Atoms",
"Nominal2_Supp",
"ExLam",
"ExLF",
"Ex1",
"Ex1rec",
"Ex2",
"Ex3",
"ExLet",
"ExLetRec",
"ExTySch",
"ExLeroy"
(* "ExCoreHaskell", *)
(* "ExPS3", *)
(* "ExPS6", *)
];