Require Import List Lia Relation_Operators.
Import ListNotations.
Require Import Undecidability.SystemF.SysF.
From Undecidability.SystemF.Util Require Import Facts poly_type_facts pure_term_facts term_facts typing_facts pure_typing_facts.

Require Import ssreflect ssrbool ssrfun.

Set Default Proof Using "Type".
Set Default Goal Selector "!".

Module Argument.
Section SysF_TYP_to_SysF_TC.

Variables : pure_term.

Definition Gamma_M0 := [poly_abs (poly_var 0)].

Definition M_M0 := pure_app (pure_var 0) (many_pure_term_abs (pure_var_bound ) ).

Definition t_M0 := poly_var 0.


Lemma transport :
  SysF_TYP SysF_TC (Gamma_M0, M_M0, t_M0).
Proof.
  move [] [t] /pure_typing_iff_type_assignment.
  move /pure_typableI /pure_typable_many_pure_term_abs_allI [{}t].
  move /(pure_typing_ren_pure_term id ( := Gamma_M0)). rewrite ren_pure_term_id.
  apply: unnest; first by case.
  move /(pure_typing_pure_app_simpleI (M := pure_var 0) (t := t_M0)).
  apply: unnest.
  { apply: (pure_typing_pure_var 0); first by reflexivity.
    apply: rt_step. by apply: contains_step_subst. }
  move /pure_typing_to_typing /= [P] [HP] /typing_to_type_assignment.
  by rewrite -HP.
Qed.


Lemma inverse_transport :
  SysF_TC (Gamma_M0, M_M0, t_M0) SysF_TYP .
Proof.
  move /pure_typing_iff_type_assignment. rewrite /Gamma_M0 /M_M0 /t_M0.
  move /pure_typingE' [?] [?] [_] [/pure_typableI _].
  have : Gamma, pure_typable .
  {
    elim: (pure_var_bound ) ([poly_abs (poly_var 0)]) .
    - move /= ? ?. eexists. by eassumption.
    - by move {}n IH /= /pure_typableE [?] /IH.
  }
  move [] [t] /pure_typing_to_typing [P] [].
  move /typing_to_type_assignment ?. by exists , t.
Qed.


End SysF_TYP_to_SysF_TC.
End Argument.

Require Import Undecidability.Synthetic.Definitions.

Theorem reduction : SysF_TYP SysF_TC.
Proof.
  exists ( 'M0 (Argument.Gamma_M0, Argument.M_M0 , Argument.t_M0)).
  move . constructor.
  - exact: Argument.transport.
  - exact: Argument.inverse_transport.
Qed.