`check_equiv` fails to check provably equal terms

[gebner]

In Pulse, we're using check_equiv to check the equality of various things, including slprops. But it seems that check_equiv only does a very limited form of equality checking (unifiability?).

module EquivTrueFalse
module T = FStar.Tactics.V2

let foo (p: squash (true == false)) =
  // assert (true == false); // ok
  assert true == false by (
    let g = T.top_env () in
    match T.check_equiv g (`(true)) (`(false)) with
    | Some tok, _ -> T.tadmit ()
    | None, issues -> T.log_issues issues; T.fail "cannot prove equality"
  )

// fails with:
// check_relation failed:  Eq ()
//     - (not equatable) not equal terms: true <> false

cc @mtzguido Is this intentional?