Goal:
  
  A : Type
  B : Type
  eqA : A -> A -> bool
  eqB : B -> B -> bool
  eqA_refl : forall a : A, eqA a a
  eqB_refl : forall b : B, eqB b b
  a : A
  b : B
  ============================
   (is_true (if eqA a a then eqB b b else false))


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrrewrite@0> $1 $2

COQC theories/MCCompare.v