Simple deduced steps

[sankalpgambhir]

Adding several deduced steps and simplifications to make proofs easier one by one.

Current additions:

• PartialCut : Perform a cut if the pivot is inside a conjunction in the conclusion
• Left{And, Or, Implies, Iff, Not, Exists, ExistsOne} : Allow usage without an argument list to infer all the parameters, given the conclusion sequent
• Right{And, Or, Implies, Iff, Not, Forall, ExistsOne} : as above ^^
• LeftForall : In lieu of a unification algorithm, reduced usage to LeftForall(termToBind: Term)
• RightExists : as above ^^

Structural steps:

• {Left, Right}Refl : Allow usage without argument list

They may be used in proofs, for example, as (sequents omitted for readability and replaced with ...):

THEOREM("example") of "..." NPROOF {
        val s0 = andThen(...)                by Weakening
        have(...)                            by Trivial
        val s1 = andThen(...)                by InstantiateForall(z)
        have(...)                            by Cut(s0, s1)
        val s2 = andThen(...)                by Weakening
        have(...)                            by LeftAnd(s2)
        andThen(...)                         by LeftNot()
        andThen(...)                         by LeftForall(z)
        andThen(...)                         by RightImplies
        andThen(...)                         by RightNot
}

As in the example, if an argument list is not required, the usages by LeftNot and by LeftNot() are equivalent.