let are_terms_variants (_term1: term) (_term2: term) : bool =

  (* acc keeps track of the bijective mapping
     from the variables of _term1 to the variables of _term2 *)
  let rec do_variants (acc: (var * var) list) (term1: term) (term2: term) :
    (var * var) list =
    
    match term1, term2 with
      | Var var1, Var var2 when
          Var.is_universal var1 == Var.is_universal var2 ->
          Tools.mapping_extend acc Var.equal Var.equal var1 var2
              
      | Const symbol1, Const symbol2 when
          Symbol.equal symbol1 symbol2 ->
          acc
              
      | Func func1, Func func2 when
          Symbol.equal func1.symbol func2.symbol ->
          Tools.array_fold2 do_variants acc func1.subterms func2.subterms
              
      | _ ->
          raise Exit
  in            
    (term_equal _term1 _term2)
    ||
    (
      try
        ignore (do_variants [] _term1 _term2);
        true
      with
        | Exit ->
            false
    )