Got the translator building

Added an extra clause to Equality type that

(!x1 v1 x2 v2. abs x1 v1 ∧ abs x2 v2 ⇒ types_match v1 v2)

where types_match is defined as

val types_match_def = tDefine "types_match" `
(types_match (Litv l1) (Litv l2) = T) ∧
(types_match (Loc loc1) (Loc loc2) = T) ∧
(types_match (Conv cn1 vs1) (Conv cn2 vs2) =
  if cn1 = cn2 then
    types_match_list vs1 vs2
  else
    F) ∧
(types_match (Closure env1 x1 e1) (Closure env2 x2 e2) = F) ∧
(types_match (Closure env1 x1 e1) (Recclosure env2 funs2 x2) = F) ∧
(types_match (Recclosure env1 funs1 x1) (Closure env2 x2 e2) = F) ∧
(types_match (Recclosure env1 funs1 x1) (Recclosure env2 funs2 x2) = F)
∧
(types_match _ _ = F) ∧
(types_match_list [] [] = T) ∧
(types_match_list (v1::vs1) (v2::vs2) =
  (types_match v1 v2 ∧ types_match_list vs1 vs2)) ∧
(* We could change this case to T, or change the semantics to have a
type error
 * when equality reaches unequal-length lists *)
(types_match_list _ _ = F)` (
 WF_REL_TAC `measure (\x. case x of INL (v1,v2) => v_size v1 | INR
(vs1,vs2) => v3_size vs1)`);

I think my previous change of equality on unequal lengths lists from
type error to false was unnecessary, but I don't want to change it back
without a reason to.

The translator seems to build the prelude script, but I don't believe
it, something must be wrong.