Add support for mutually recursive datatypes to the translator

[myreen]

This issue is about extending the translator with support for mutually recursive datatypes. Below is a target example, which currently fails due to limitations of the translator's register_type function.

Datatype:
  a = A1 | A2 b ;
  b = B1 | B2 a
End

Definition is_A1_def:
  is_A1 A1 = T ∧
  is_A1 _  = F
End

Definition a_len_def:
  a_len A1 = 0n ∧
  a_len (A2 b) = 1 + b_len b ∧
  b_len B1 = 0 ∧
  b_len (B2 a) = 1 + a_len a
End

val r = translate is_A1_def;
val r = translate a_len_def;