<sarcastic> sounds like fun </sarcastic> Unlike Qi I, Qi II allows you to embed sequent rules within functions, evaluating them to closures. These rule closure

<sarcastic> sounds like fun </sarcastic> Unlike Qi I, Qi II allows you to embed sequent rules within functions, evaluating them to closures. These rule closures are type checked and are permeable to having their variables lexically bound from outside the scope of the rule itself. These devices enable the student of computational logic to effortlessly code complex logical systems of all descriptions. Thus the rule let PTerm/X (replace-by X Term P) PTerm/X, (all X P) >> Q; ____________________ (all X P) >> Q; allows universally quantified assumptions to be instantiated to new premises. This rule can be embedded into a Qi II function called all-left which does precisely this job. The rule is turned into a closure by the rule function which is then applied to the problem (list of sequents). (define all-left {term --> [sequent] --> [sequent]} Term S -> ((rule let PTerm/X (replace-by X Term P) PTerm/X, (all X P) >> Q; ____________________ (all X P) >> Q;) S))