refactor: is_trivial check to be more succinct

[Equilibris]

If we start with

let is_trivial :=
  args.length == arity
  && args.toList.enum.all fun ⟨i, arg⟩ =>
      arg.isFVar && isLiveVar vars arg.fvarId! && vars'.indexOf arg.fvarId! == i

Then we can first observe that
vars'.indexOf arg.fvarId! == i => isLiveVar vars arg.fvarId!.
this comes from indexOf returning the length of the array if the entry is not found.
Since 0 ≤ i < vars'.legnth we can never have i == vars'.length thereby the impl holds
so we can remove the isLive check

let is_trivial :=
  args.length == arity
  && args.toList.enum.all fun ⟨i, arg⟩ =>
      arg.isFVar && vars'.indexOf arg.fvarId! == i

Then we can re-arrange to take the transform for fvarIds out

let is_trivial :=
  args.length == arity
  && (args.toList.mapM Expr.fvarId?).any
    (·.enum.all fun ⟨i, arg⟩ => vars'.indexOf arg == i)

Now observe how we are checking an index at each step along the way.
If the arrays have the same length (the first check) we then know if they are equal this holds.
So by doing the next transform we get:

let is_trivial :=
  args.length == arity
  && (args.toList.mapM Expr.fvarId?).any (· == vars')

And finally if the arrays are equal it implies the first condition so we end up with:

let is_trivial := (args.toList.mapM Expr.fvarId?).any (· == vars')

Which happends to also correspond to what the documentation states

[alexkeizer]

LGTM, feel free to merge after #22 goes through