New tactic trait system interferes with overload resolution

[sankalpgambhir]

The ParameterlessAndThen trait supplies an apply function with the signature Fact => (Sequent => Judgement). However, several tactics implement also an overloaded version of apply. For example, with LeftAnd, apply :: Formula => Formula => (Fact => (Sequent => Judgement)). Calling LeftAnd(phi, psi) per this overloaded raises an error:

[error] 26 |      andThen(...) by LeftAnd(P(x), P(x))
[error]    |                             ^^^^^^^^
[error]    |    Found:    (lisa.kernel.fol.FOL.Formula, lisa.kernel.fol.FOL.Formula)
[error]    |    Required: evidence$3.Fact

Small proof to get this error:

val testThm = makeTHM("('P('x) ⇒ 'P('f('x))) /\\ 'P('x) ⊢ 'P('x) ⇒ 'P('f('x))") {
    val i1 = have(P(x) ==> P(f(x)) |- P(x) ==> P(f(x))) by Restate;
    have(P(x) ==> P(f(x)) |- P(x) ==> P(f(x))) by Restate(i1)
    andThen((P(x) ==> P(f(x))) /\ P(x) |- P(x) ==> P(f(x))) by LeftAnd(P(x) ==> P(f(x)), P(x))
  }
  show

It seems that due to the trait, the overloaded apply method is not visible.

[sankalpgambhir]

Should be addressed with #101.