From Undecidability.L.Tactics Require Import LTactics GenEncode.

Set Default Proof Using "Type".

Section Fix_X.
  Variable (X:Type).
  Context {intX : encodable X}.

  MetaCoq Run (tmGenEncode "list_enc" (list X)).

  Global Instance encInj_list_enc {H : encInj intX} : encInj (encodable_list_enc).
  Proof. register_inj. Qed.


  Global Instance termT_cons : computableTime' (@cons X) (fun a aT => (1,fun A AT => (1,tt))).
  Proof.
    extract constructor.
    solverec.
  Qed.
End Fix_X.

Hint Resolve list_enc_correct : Lrewrite.