theory Sequent1 imports "FOL_Seq_Calc1.Sequent" begin text ‹This theory exists exclusively as a shim to link the AFP theory imported here to the ‹Sequent_Calculus_Verifier› theory.› end