GADTs have become a common feature of strongly typed functional programming languages. They are often presented as a weaker form of the inductive types seen in Coq or Agda. In both cases, constraints generated by pattern-matching allow one to generate equations that can be applied to types. However, there is an important difference: in OCaml or Haskell, unification can be used to refine syntactic equations on types, while this is not the case in Coq or Agda, where one cannot observe that type constructors are syntactically injective. This is a problem when one wants to translate code from a functional programming language to a type-theory based proof assistant, as a literal translation would not allow one to infer the necessary equations. This may be one of the reasons why existing automatic translators provide little or no support for GADTs. In this presentation we show how to avoid this problem by using a two-pronged translation, where OCaml types are mapped to an intensional representation, that preserves the deductive properties, which is itself interpreted into concrete Coq types, that allow computation. We also discuss what is further needed for an automatic translator.