(* First-Order Logic with Natural Deduction *) use_thys ["FOL"];