Require Import List Lia.
Import ListNotations.
Require Import Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax.
From Undecidability.SystemF.Util Require Import Facts poly_type_facts term_facts typing_facts iipc2_facts sn_facts.

Require Import Undecidability.DiophantineConstraints.H10C.

Require Import ssreflect ssrbool ssrfun.

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

Local Arguments nth_error_In {A l n x}.
Local Arguments In_nth_error {A l x}.
Local Arguments Forall_inv {A P a l}.
Local Arguments Forall_inv_tail {A P a l}.

Module SafePolyType.
Local Fixpoint is_safe_poly_arr (n: ) (t: poly_type) :=
  match t with
  | poly_var x n x
  | poly_arr _ t is_safe_poly_arr n t
  | poly_abs _ False
  end.

Fixpoint is_safe_poly_type (n: ) (t: poly_type) :=
  if t is poly_abs t then is_safe_poly_type (1+n) t else is_safe_poly_arr n t.

Definition safe_poly_type (n: ) (ts: list poly_type) (x: ) :=
  many_poly_abs n (many_poly_arr ts (poly_var (n + x))).

Lemma safe_poly_type_eqE {n n' ts ts' x x'} : safe_poly_type n ts x = safe_poly_type n' ts' x'
  n = n' ts = ts' x = x'.
Proof.
  elim: n n' x x'.
  - move [|?]; last by case: ts.
    move x x'. elim: ts ts'.
    + case; last done. by move [].
    + move ? ? IH. case; first done.
      by move ? ? [] /IH [_] [] .
  - move n IH [|n']; first by case: (ts'). move x x' [].
    have : S (n + x) = n + (S x) by . have : S (n' + x') = n' + (S x') by .
    by move /IH [] [] [].
Qed.


Lemma is_safe_poly_arrE {i t} : is_safe_poly_arr i t
   (ts : list poly_type) (x : ), t = (many_poly_arr ts (poly_var (i+x))).
Proof.
  elim: t.
  - move /= x *. exists [], (x-i). congr poly_var. by .
  - move s _ ? IH /= /IH [ts] [x] . by exists (s :: ts), x.
  - done.
Qed.


Lemma is_safe_poly_typeE {i t} : is_safe_poly_type i t
   (n : ) (ts : list poly_type) (x : ),
    t = many_poly_abs n (many_poly_arr ts (poly_var (n + (i + x)))).
Proof.
  elim: t i.
  - move /= x i *. exists 0, [], (x-i). congr poly_var. by .
  - move s _ t _ ? /= /is_safe_poly_arrE [ts] [x] .
    by exists 0, (s :: ts), x.
  - move ? IH i /IH [n] [ts] [x] . exists (1+n), ts, x.
    move /=. do 4 f_equal. by .
Qed.


Lemma typing_safe_poly_typeE {Gamma P n ss x As y} :
  typing P (many_poly_abs n (many_poly_arr ss (poly_var (n+x))))
  typing (many_argument_app P As) (poly_var y)
   (ts : list poly_type) (Qs : list term),
    x = y
    As = (map argument_poly_type ts) (map argument_term Qs)
    n = length ts
    length ss = length Qs.
Proof.
  elim: n P ss x As.
  - move P ss x As /=. elim: ss P As.
    + move P [| [?|?] ?].
      * move /typing_functional H /H [] . by exists [], [].
      * move /= + /typing_many_argument_subterm [?] /typingE [?].
        by move /typing_functional H [/H].
      * move /= + /typing_many_argument_subterm [?] /typingE [?].
        by move /typing_functional H [_ /H].
    + move s ss IH P [| [Q|?] ?] /=.
      * by move /typing_functional H /H.
      * move + /copy [/IH {}IH].
        move + /typing_many_argument_subterm [?] /copy [/typingE [?]].
        move /typing_functional H [/H{H} []] ? /IH.
        move [[| ? ?]] [Qs] [] [] [?] ; last done. by exists [], (Q :: Qs).
      * move + /typing_many_argument_subterm [?] /typingE [?].
        by move /typing_functional H [_ /H].
  - move n IH P ss x [|A As] /=.
    + by move /typing_functional H /H.
    + move: A [? | s].
      * move + /typing_many_argument_subterm [?] /typingE [?].
        by move /typing_functional H [/H].
      * move /typing_ty_app /(_ s). rewrite subst_poly_type_many_poly_abs subst_poly_type_many_poly_arr /=.
        have : S (n + x) = n + S x by . rewrite iter_up_poly_type_poly_type.
        move /IH {}IH /IH. move [ts] [Qs] [] [] [].
        rewrite map_length. move . by exists (s :: ts), Qs.
Qed.


Lemma typing_is_safe_environment {Gamma P x} : normal_form P typing P (poly_var x)
  Forall (is_safe_poly_type 0)
   ss y ts Qs,
    P = many_app (many_ty_app (var y) ts) Qs
    nth_error y = Some (safe_poly_type (length ts) ss x)
     (typing ) Qs (map (subst_poly_type (fold_right scons poly_var (rev ts))) ss).
Proof.
  case; [ | by move > _ /typingE [?] [] | by move > _ /typingE [?] []].
  move {}P /many_argument_appI [y] [As] [ _].
  move /copy [/typing_many_argument_subterm [?]]. move /copy [/typingE].
  move + + + /Forall_forall H /nth_error_In /H{H} /is_safe_poly_typeE.
  move [n] [ss] [z] Hy HyAs. exists ss, y.
  move: (Hy) (HyAs) /typing_safe_poly_typeE H /H{H}.
  move [ts] [Qs] [?] [?] [? ?]. exists ts, Qs. subst x As.
  subst n. constructor; [|constructor].
  - by rewrite many_argument_app_app many_argument_app_map_argument_poly_type many_argument_app_map_argument_term.
  - by move: Hy /typingE.
  - move: Hy /typing_many_ty_appI /(_ ts ltac:()).
    move: HyAs. rewrite many_argument_app_app many_argument_app_map_argument_poly_type.
    move: (many_ty_app (var y) _) {}P.
    rewrite subst_poly_type_many_poly_arr many_argument_app_map_argument_term.
    move /typing_many_app_arguments H /H. apply. by rewrite map_length.
Qed.


Corollary iipc2_is_safe_environment {Gamma x} : (poly_var x) Forall (is_safe_poly_type 0)
   ss ts,
    In (safe_poly_type (length ts) ss x)
    Forall ( ) (map (subst_poly_type (fold_right scons poly_var (rev ts))) ss).
Proof.
  move [P] /typing_normal_form [{}P] [/typing_is_safe_environment H] /H {}H /H.
  move [ss] [?] [ts] [?] [_] [/nth_error_In ?] /Forall2_typing_Forall_iipc2 ?.
  by exists ss, ts.
Qed.


Lemma last_poly_var_safe_poly_type {t n ss x} : t = safe_poly_type n ss x last_poly_var t = Some x.
Proof.
  move . elim: n ss x.
  - move + x. by elim.
  - move n /= + ss x. have : S (n + x) = n + S x by . by move .
Qed.


Lemma parameters_poly_arr_safe_poly_type {n ss x}:
  parameters_poly_arr (safe_poly_type n ss x) = if n is 0 then ss else [].
Proof.
  case: n; last done.
  elim: ss; first done. by move /= ? ? .
Qed.


Lemma safe_poly_typeP {n ss x} : is_safe_poly_type 0 (safe_poly_type n ss x).
Proof.
  have : x = 0 + x by . move: (0) k. elim: n k.
  - move k. elim: ss; [move /=; by | by move /= ? [|? ?]].
  - move n IH k /=. have : S (n + (k + x)) = n + ((S k) + x) by .
    by apply: IH.
Qed.

End SafePolyType.

Module Argument.
Import SafePolyType.

Section H10C_SAT_to_SysF_INH.

Variable h10cs : list h10c.
Fixpoint variable_bound (h10cs : list h10c) : :=
  match h10cs with
  | [] 0
  | (h10c_one x) :: h10cs 1 + x + variable_bound h10cs
  | (h10c_plus x y z) :: h10cs 1 + x + y + z + variable_bound h10cs
  | (h10c_mult x y z) :: h10cs 1 + x + y + z + variable_bound h10cs
  end.

Definition δ := variable_bound h10cs.
Lemma δP :
  Forall ( c
    match c with
    | (h10c_one x) x < δ
    | (h10c_plus x y z) x < δ y < δ z < δ
    | (h10c_mult x y z) x < δ y < δ z < δ
    end) h10cs.
Proof.
  rewrite /δ. elim: (h10cs); first by constructor.
  move c cs IH. constructor.
  - case: c /= *; by .
  - apply: Forall_impl IH. move: c + []; case > /=; by .
Qed.


Definition tt := 0. Definition ut := 1.
Definition st := 2.
Definition pt := 3.
Definition b1t := 4.
Definition b2t := 5.
Definition b3t := 6.
Definition GammaC := map poly_var (seq 0 7).
Arguments GammaC : simpl never.

Definition dt := 7.
Definition to_d' d (t: poly_type) := poly_arr t (poly_var (d+dt)).
Definition to_d := to_d' 0.

Definition Ut' d t := many_poly_arr [poly_arr (to_d' d t) (poly_var (d+b1t)); poly_arr t (poly_var (d+b2t))] (poly_var (d+ut)).
Definition Ut := Ut' 0.

Definition St' d := '(t1, t2, t3)
  many_poly_arr [poly_arr (to_d' d ) (poly_var (d+b1t)); poly_arr (to_d' d ) (poly_var (d+b2t)); poly_arr (to_d' d ) (poly_var (d+b3t))] (poly_var (d+st)).
Definition St := St' 0.

Definition Pt' d := '(t1, t2, t3)
  many_poly_arr [poly_arr (to_d' d ) (poly_var (d+b1t)); poly_arr (to_d' d ) (poly_var (d+b2t)); poly_arr (to_d' d ) (poly_var (d+b3t))] (poly_var (d+pt)).
Definition Pt := Pt' 0.

Definition zt' d := d + 10.
Definition zt := zt' 0.
Definition t_u :=
  poly_abs (many_poly_arr [
    Ut' 1 (poly_var 0);
    Ut' 1 (poly_var 0);
    Ut' 1 (poly_var 0);
    Ut' 1 (poly_var 0);
    poly_abs (many_poly_arr [
      Ut' 2 (poly_var 0);
      St' 2 ((poly_var 1), (poly_var (1+ zt' 2)), (poly_var 0));
      St' 2 ((poly_var 0), (poly_var (0+ zt' 2)), (poly_var 0));
      Pt' 2 ((poly_var 0), (poly_var (0+ zt' 2)), (poly_var (0+ zt' 2)))
    ] (poly_var (2+tt)))
  ] (poly_var (1+tt))).

Definition t_s :=
  many_poly_abs 5 (many_poly_arr [
    poly_arr (St' 5 ((poly_var 0), (poly_var 3), (poly_var 4))) (poly_var (5+tt));
    Ut' 5 (poly_var 0); Ut' 5 (poly_var 1); Ut' 5 (poly_var 2); Ut' 5 (poly_var 3); Ut' 5 (poly_var 4);
    St' 5 ((poly_var 0), (poly_var 1), (poly_var 2));
    St' 5 ((poly_var 1), (poly_var (1 + zt' 5)), (poly_var 3));
    St' 5 ((poly_var 2), (poly_var (1 + zt' 5)), (poly_var 4))
  ] (poly_var (5+tt))).

Definition t_p :=
  many_poly_abs 5 (many_poly_arr [
    poly_arr (Pt' 5 ((poly_var 0), (poly_var 3), (poly_var 4))) (poly_var (5+tt));
    Ut' 5 (poly_var 0); Ut' 5 (poly_var 1); Ut' 5 (poly_var 2); Ut' 5 (poly_var 3); Ut' 5 (poly_var 4);
    Pt' 5 ((poly_var 0), (poly_var 1), (poly_var 2));
    St' 5 ((poly_var 1), (poly_var (1 + zt' 5)), (poly_var 3));
    St' 5 ((poly_var 2), (poly_var 0), (poly_var 4))
  ] (poly_var (5+tt))).

Definition h10c_poly_type (c: h10c) : poly_type :=
  match c with
  | (h10c_one x) St' δ (poly_var x, poly_var (δ + zt), poly_var (δ+1+zt))
  | (h10c_plus x y z) St' δ (poly_var x, poly_var y, poly_var z)
  | (h10c_mult x y z) Pt' δ (poly_var x, poly_var y, poly_var z)
  end.

Definition t_cs :=
  many_poly_abs δ (many_poly_arr (map ( x Ut' δ (poly_var x)) (seq 0 δ) map h10c_poly_type h10cs) (poly_var (δ + tt))).

Definition := [t_u; t_s; t_p; t_cs].

Definition GammaH :=
  (map Ut (map ( x poly_var (x + zt)) [0; 1]))
  (map St [
    (poly_var zt, poly_var zt, poly_var zt);
    (poly_var (1+zt), poly_var zt, poly_var (1+zt));
    (poly_var zt, poly_var (1+zt), poly_var (1+zt))])
  (map Pt [(poly_var zt, poly_var zt, poly_var zt); (poly_var (1+zt), poly_var zt, poly_var zt)]).

Arguments : simpl never.
Arguments Ut' : simpl never.
Arguments St' : simpl never. Arguments St : simpl never.
Arguments Pt' : simpl never. Arguments Pt : simpl never.

Definition encodes_nat (t: poly_type) (n: ) :=
   GammaC (poly_arr (to_d (poly_var (n + zt))) (to_d t))
   GammaC (poly_arr (to_d t) (to_d (poly_var (n + zt)))).

Definition encodes_sum := '(t1, t2, t3)
   n1 n2 n3, encodes_nat encodes_nat encodes_nat + = .

Definition encodes_prod := '(t1, t2, t3)
   n1 n2 n3, encodes_nat encodes_nat encodes_nat * = .

Lemma is_safe_environment_Gamma0 : Forall (is_safe_poly_type 0) .
Proof.
  do 3 (constructor; first by move /=; ).
  constructor; [by apply: safe_poly_typeP | done].
Qed.


Lemma is_safe_environment_Ut {ts} : Forall (is_safe_poly_type 0) (map Ut ts).
Proof. apply /Forall_mapP /Forall_forall ? _ /=. by . Qed.

Lemma is_safe_environment_St {tSs} : Forall (is_safe_poly_type 0) (map St tSs).
Proof. apply /Forall_mapP /Forall_forall [[[? ?] ?]] _ /=. by . Qed.

Lemma is_safe_environment_Pt {tPs} : Forall (is_safe_poly_type 0) (map Pt tPs).
Proof. apply /Forall_mapP /Forall_forall [[[? ?] ?]] _ /=. by . Qed.

Lemma iipc2_to_dE {x y: } : dt < x dt < y
   GammaC (poly_arr (to_d (poly_var x)) (to_d (poly_var y)))
  x = y.
Proof.
  move Hx Hy /iipc2_poly_arrE /iipc2_poly_arrE /iipc2_is_safe_environment.
  move [:HGamma]. rewrite [GammaC]lock. apply: unnest.
  { abstract: HGamma. rewrite -lock. by do ? (constructor; first by move /=; ). }
  move [ss] [ts] /= []. move [| [|]].
  - move /last_poly_var_safe_poly_type []. by .
  - have : to_d (poly_var x) = safe_poly_type 0 [poly_var x] dt by done.
    move /safe_poly_type_eqE [+] [ _]. case: ts; last done.
    move _ /Forall_inv /iipc2_is_safe_environment /(_ HGamma).
    move [ss'] [ts'] /= []. move [| [|]].
    + by move /last_poly_var_safe_poly_type [] .
    + move /safe_poly_type_eqE. by .
    + rewrite -lock /GammaC in_map_iff [[?]] [+].
      move /last_poly_var_safe_poly_type [] /in_seq. move: Hx. rewrite /dt. by .
  - rewrite -lock /GammaC. move /in_map_iff [?] [].
    move /last_poly_var_safe_poly_type [] /in_seq. move: Hx. rewrite /dt. by .
Qed.


Lemma to_d_typingI s t Gamma : (poly_arr (poly_arr s t) (poly_arr (to_d t) (to_d s))).
Proof.
  eexists. apply /typing_abs /typing_abs /typing_abs /typing_app.
  - apply: (typing_var (x := 1)). by reflexivity.
  - apply: typing_app.
    + apply: (typing_var (x := 2)). by reflexivity.
    + apply: (typing_var (x := 0)). by reflexivity.
Qed.


Lemma encodes_natI (n: ) : encodes_nat (poly_var (n + zt)) n.
Proof. constructor; eexists; apply: typing_abs; by apply: (typing_var (x := 0)). Qed.

Lemma encodes_nat_transport {s t n n'} : GammaC (poly_arr (to_d s) (to_d t))
  encodes_nat s n encodes_nat t n' n = n'.
Proof.
  move + [Hn _] [_ Hn'].
  move: Hn /iipc2_poly_arr_comp H /H{H}.
  move: Hn' + /iipc2_poly_arr_comp H /H{H} /iipc2_to_dE.
  rewrite /dt /zt /zt'. by .
Qed.


Lemma subst_poly_type_Ut' {ts t} : let σ := fold_right scons poly_var ts in
  subst_poly_type σ (Ut' (length ts) t) = Ut (subst_poly_type σ t).
Proof. by rewrite /= ?fold_right_length_ts. Qed.

Lemma subst_poly_type_St' {ts t1 t2 t3} : let σ := fold_right scons poly_var ts in
  subst_poly_type σ (St' (length ts) (, , )) = St (subst_poly_type σ , subst_poly_type σ , subst_poly_type σ ).
Proof. by rewrite /= ?fold_right_length_ts. Qed.

Lemma subst_poly_type_Pt' {ts t1 t2 t3} : let σ := fold_right scons poly_var ts in
  subst_poly_type σ (Pt' (length ts) (, , )) = Pt (subst_poly_type σ , subst_poly_type σ , subst_poly_type σ ).
Proof. by rewrite /= ?fold_right_length_ts. Qed.

Lemma last_poly_var_t_cs : last_poly_var t_cs = Some tt.
Proof.
  rewrite /t_cs. move: (_ _) ss. move: (tt) x.
  elim: (δ) x.
  - move x. by elim: ss.
  - move n + x /=. have : S (n + x) = n + S x by . by move .
Qed.


Lemma generalize_Gamma0 {GammaU GammaS GammaP t} : ( GammaU GammaS GammaP) t
   ([poly_var tt] GammaU GammaS GammaP) t.
Proof.
  move: (GammaU GammaS GammaP) ?. apply: iipc2_generalization.
  do 3 (constructor; first by (apply: last_poly_var_typingI; left)).
  constructor; first by (apply: last_poly_var_typingI; rewrite last_poly_var_t_cs; left).
  by apply /Forall_forall ? ?; apply /iipc2_var_InI /in_app_r.
Qed.


Lemma generalize_GammaU {Gamma GammaS GammaP tUs t} : ( map Ut tUs GammaS GammaP) t
   ( [poly_var ut] GammaS GammaP) t.
Proof.
  move: (GammaS GammaP) GammaSP. apply: iipc2_generalization.
  apply /Forall_forall ?.
  case /in_app_iff; first by (move ?; apply: iipc2_var_InI; rewrite ?in_app_iff; tauto).
  case /in_app_iff; last by (move ?; apply: iipc2_var_InI; rewrite ?in_app_iff; tauto).
  move /in_map_iff [?] [ _]. apply /last_poly_var_typingI /in_app_r. by left.
Qed.


Lemma generalize_GammaS {Gamma GammaU GammaP tSs t} : ( GammaU map St tSs GammaP) t
   ( GammaU [poly_var st] GammaP) t.
Proof.
  apply: iipc2_generalization. apply /Forall_forall ?.
  case /in_app_iff; first by (move ?; apply: iipc2_var_InI; rewrite ?in_app_iff; tauto).
  case /in_app_iff; first by (move ?; apply: iipc2_var_InI; rewrite ?in_app_iff; tauto).
  case /in_app_iff; last by (move ?; apply: iipc2_var_InI; rewrite ?in_app_iff; tauto).
  move /in_map_iff [[[? ?]?]] [ _]. apply /last_poly_var_typingI /in_app_r /in_app_r. by left.
Qed.


Lemma generalize_GammaP {Gamma GammaU GammaS tPs t} : ( GammaU GammaS map Pt tPs ) t
   ( GammaU GammaS [poly_var pt]) t.
Proof.
  apply: iipc2_generalization. apply /Forall_forall ?.
  do 3 (case /in_app_iff; first by (move ?; apply: iipc2_var_InI; rewrite ?in_app_iff; tauto)).
  move /in_map_iff [[[? ?]?]] [ _]. apply /last_poly_var_typingI /in_app_r /in_app_r /in_app_r. by left.
Qed.


Lemma subst_poly_type_h10c_poly_type {ts c} : let σ := (fold_right scons poly_var (rev ts)) in δ = length ts
  subst_poly_type σ (h10c_poly_type c) =
    match c with
    | (h10c_one x) St (σ x, poly_var zt, poly_var (1+zt))
    | (h10c_plus x y z) St (σ x, σ y, σ z)
    | (h10c_mult x y z) Pt (σ x, σ y, σ z)
    end.
Proof.
  move σ Hts. subst σ. case: c.
  - move x. rewrite /= Hts -rev_length ?fold_right_length_ts.
    have : length (rev ts) + 1 + zt = length (rev ts) + (1 + zt) by .
    by rewrite fold_right_length_ts.
  - move >. by rewrite /= Hts -rev_length ?fold_right_length_ts.
  - move >. by rewrite /= Hts -rev_length ?fold_right_length_ts.
Qed.


Section InverseTransport.
Lemma iipc2_Ut_unique {xs tSs tPs t} :
   ( map Ut (map ( x : poly_var (x + zt)) xs) map St tSs map Pt tPs) (Ut t)
   n, encodes_nat t n.
Proof.
  move /generalize_Gamma0 /generalize_GammaS /generalize_GammaP.
  move /iipc2_poly_arrE /iipc2_poly_arrE /iipc2_is_safe_environment. apply: unnest.
  {
    do 3 (constructor; first by move /=; ).
    apply: Forall_appI; first by apply: is_safe_environment_Ut.
    by do 2 (constructor; first by move /=; ).
  }
  rewrite [[poly_var tt]]lock [[poly_var st]]lock [[poly_var pt]]lock.
  move [ss'] [ts'] [+ Hss] /=. rewrite -lock /= in_app_iff in_map_iff /=.
  do 3 (case; first by move /last_poly_var_safe_poly_type).
  case; first last.
  { unlock. do 2 (case; first by move /last_poly_var_safe_poly_type). done. }
  move [tx]. rewrite in_map_iff. move [Hx] [x] [?] Hxxs. subst tx. exists x.
  move: Hx Hss /( parameters_poly_arr). rewrite parameters_poly_arr_safe_poly_type /=.
  case: ts'; last done. move /= . rewrite ?app_comm_cons.
  move /Forall_consP [+ /Forall_consP [+ _]]. rewrite ?subst_poly_type_poly_var.
  unlock. move /generalize_GammaU /generalize_GammaU . constructor.
  -
    move: /iipc2_poly_arrE /iipc2_is_safe_environment. clear. apply: unnest.
    { by do ? (constructor; first by move /=; ). }
    move [ss] [ts] /= [].
    do 2 (case; first by move /last_poly_var_safe_poly_type).
    case; first last.
    { do 4 (case; first by move /last_poly_var_safe_poly_type). done. }
    
    move /( parameters_poly_arr). rewrite parameters_poly_arr_safe_poly_type /=.
    case: ts; last done. move /= . move /Forall_inv [?] /typing_abs /iipc2I.
    rewrite subst_poly_type_poly_var. apply: iipc2_generalization.
    by do 6 (constructor; first by (apply: last_poly_var_typingI; firstorder done)).
  -
    have ? : x + zt b2t by (rewrite /dt /zt /zt' /b2t; ).
    move: /iipc2_poly_arrE /iipc2_is_safe_environment. apply: unnest.
    { by do ? (constructor; first by move /=; ). }
    move [ss] [ts] /= [].
    case; first by (move /last_poly_var_safe_poly_type; case).
    case; first last.
    { do 5 (case; first by move /last_poly_var_safe_poly_type). done. }
    
    move /( parameters_poly_arr). rewrite parameters_poly_arr_safe_poly_type /=.
    case: ts; last done. move /= . move /Forall_inv [?] /typing_abs /iipc2I. clear.
    rewrite subst_poly_type_poly_var. move /iipc2_generalization /(_ GammaC). apply: unnest.
    { by do 6 (constructor; first by (apply: last_poly_var_typingI; firstorder done)). }
    move [?] /(typing_app _) H. by have [? /H /iipc2I] := to_d_typingI (poly_var (x + zt)) t GammaC.
Qed.


Lemma generalize_GammaC {s t t1 t2 t3}:
  
    (to_d s :: [poly_arr (to_d ) (poly_var b3t);
        poly_arr (to_d ) (poly_var b2t); poly_arr (to_d ) (poly_var b1t); poly_var tt]
        [poly_var ut] [poly_var st] [poly_var pt]) (to_d t)
   GammaC (poly_arr (to_d s) (to_d t)).
Proof.
  move [?] /typing_abs /iipc2I /iipc2_generalization. apply.
  by do 7 (constructor; first by (apply: last_poly_var_typingI; firstorder done)).
Qed.


Lemma encodes_nat_transport' {x s t1 t2 t3 n n1 n2 n3} :
  
    ([poly_arr (to_d ) (poly_var b3t); poly_arr (to_d ) (poly_var b2t); poly_arr (to_d ) (poly_var b1t); poly_var tt]
     [poly_var ut] [poly_var st] [poly_var pt]) (poly_arr (to_d s) (poly_var x))
  encodes_nat encodes_nat encodes_nat encodes_nat s n
  (x = b1t n = ) (x = b2t n = ) (x = b3t n = ).
Proof.
  have : (x b1t x b2t x b3t) (x = b1t) (x = b2t) (x = b3t) by .
  case; first by . move Hx.
  move /iipc2_poly_arrE /iipc2_is_safe_environment. apply: unnest.
  { by do ? (constructor; first by move /=; ). }
  move [ss] [ts] [+ Hss] /=.
  case; first by move /last_poly_var_safe_poly_type [] ?; subst x.
  case.
  {
    move /copy [/( parameters_poly_arr) + /last_poly_var_safe_poly_type [{}Hx]].
    rewrite parameters_poly_arr_safe_poly_type /=. case: ts Hss; last done. move /= + ?. subst x ss.
    move /Forall_inv. rewrite subst_poly_type_poly_var.
    by move /generalize_GammaC /encodes_nat_transport H _ _ /H {}H /H{H} .
  }
  case.
  {
    move /copy [/( parameters_poly_arr) + /last_poly_var_safe_poly_type [{}Hx]].
    rewrite parameters_poly_arr_safe_poly_type /=. case: ts Hss; last done. move /= + ?. subst x ss.
    move /Forall_inv. rewrite subst_poly_type_poly_var.
    by move /generalize_GammaC /encodes_nat_transport H _ /H {}H _ /H{H} .
  }
  case.
  {
    move /copy [/( parameters_poly_arr) + /last_poly_var_safe_poly_type [{}Hx]].
    rewrite parameters_poly_arr_safe_poly_type /=. case: ts Hss; last done. move /= + ?. subst x ss.
    move /Forall_inv. rewrite subst_poly_type_poly_var.
    by move /generalize_GammaC /encodes_nat_transport H /H {}H _ _ /H{H} .
  }
  by do 4 (case; first by move /last_poly_var_safe_poly_type [] ?; subst x).
Qed.


Lemma iipc2_St_soundness {xs tSs tPs t1 t2 t3 n1 n2 n3} :
   ( map Ut (map ( x : poly_var (x + zt)) xs) map St tSs map Pt tPs) (St (, , ))
  Forall encodes_sum tSs encodes_nat encodes_nat encodes_nat + = .
Proof.
  move /generalize_Gamma0 /generalize_GammaU /generalize_GammaP.
  move + HtSs /= /iipc2_poly_arrE /iipc2_poly_arrE /iipc2_poly_arrE /iipc2_is_safe_environment. apply: unnest.
  {
    do 5 (constructor; first by move /=; ).
    apply: Forall_appI; first by apply: is_safe_environment_St.
    by (constructor; first by move /=; ).
  }
  move [ss'] [ts'] [+ Hss] /=.
  do 5 (case; first by move /last_poly_var_safe_poly_type).
  move /in_app_iff.
  case; last by case; [move /last_poly_var_safe_poly_type | done].
  move /in_map_iff [[[ ] ]] /= [/( parameters_poly_arr)].
  rewrite parameters_poly_arr_safe_poly_type /=.
  move Hss'. case: ts' Hss' Hss; last done.
  rewrite /length . rewrite map_subst_poly_type_poly_var ?app_comm_cons.
  move /Forall_consP [/generalize_GammaS ] /Forall_consP [/generalize_GammaS ] /Forall_consP [/generalize_GammaS ] _.
  move: HtSs /Forall_forall H /H{H} /= [] [] [] [] [] [] + .
  have := encodes_nat_transport' .
  have := encodes_nat_transport' .
  have := encodes_nat_transport' .
  clear. rewrite /b1t /b2t /b3t. by .
Qed.


Lemma iipc2_Pt_soundness {xs tSs tPs t1 t2 t3 n1 n2 n3} :
   ( map Ut (map ( x : poly_var (x + zt)) xs) map St tSs map Pt tPs) (Pt (, , ))
  Forall encodes_prod tPs encodes_nat encodes_nat encodes_nat * = .
Proof.
  move /generalize_Gamma0 /generalize_GammaU /generalize_GammaS.
  move + HtSs /= /iipc2_poly_arrE /iipc2_poly_arrE /iipc2_poly_arrE /iipc2_is_safe_environment. apply: unnest.
  {
    do 6 (constructor; first by move /=; ).
    by apply: is_safe_environment_Pt.
  }
  move [ss'] [ts'] [+ Hss] /=. rewrite in_map_iff.
  do 6 (case; first by move /last_poly_var_safe_poly_type).
  move [[[ ] ]] /= [/( parameters_poly_arr)]. rewrite parameters_poly_arr_safe_poly_type /=.
  move Hss'. case: ts' Hss' Hss; last done.
  rewrite /length . under [map (subst_poly_type _) _]map_ext ? do (rewrite subst_poly_type_poly_var).
  rewrite map_id ?app_comm_cons.
  move /Forall_consP [/generalize_GammaP ] /Forall_consP [/generalize_GammaP ] /Forall_consP [/generalize_GammaP ] _.
  move: HtSs /Forall_forall H /H{H} /= [] [] [] [] [] [] + .
  have := encodes_nat_transport' .
  have := encodes_nat_transport' .
  have := encodes_nat_transport' .
  clear. rewrite /b1t /b2t /b3t. by .
Qed.


Lemma construct_h10cs_solution {xs tSs tPs P}:
  normal_form P Forall encodes_sum tSs Forall encodes_prod tPs
  typing ( (map Ut (map ( x poly_var (x + zt)) xs)) (map St tSs) (map Pt tPs)) P (poly_var tt) H10C_SAT h10cs.
Proof using h10cs.

  elim /(measure_ind term_size): P xs tSs tPs P IH xs tSs tPs + HtSs HtPs.
  move /copy [HP] /typing_is_safe_environment H /H{H}. apply: unnest.
  {
    apply: Forall_appI; first by apply: is_safe_environment_Gamma0.
    apply: Forall_appI; first by apply: is_safe_environment_Ut.
    apply: Forall_appI; [by apply: is_safe_environment_St | by apply: is_safe_environment_Pt].
  }
  move [ss] [?] [ts] [Qs] [?] [/nth_error_In]. subst P. case /in_app_iff.
  {
    case; [|case; [|case; [|case]]]; last done.
    -
      move: IH HP. case ts; first by case: ss.
      move s. case; last by case ss.
      move IH HQs [] /( parameters_poly_arr). rewrite ?parameters_many_poly_arr. move HQsss.
      move: (HQsss) /Forall2_length_eq /=. move HQs': (Qs) Qs'.
      move: Qs' HQs' [|]; first done.
      move [|]; first done. move [|]; first done. move [|]; first done. move [|]; first done.
      move [|]; last done. move ? _. subst Qs.
      move: HQs /normal_form_many_app [_ +]. do 4 (move /Forall_inv_tail). move /Forall_inv .
      move: HQsss /Forall2_consE [/iipc2I ] /Forall2_consE [_] /Forall2_consE [_] /Forall2_consE [_] /Forall2_consE [+ _].
      have [n Hsn] : n, encodes_nat s n by apply: iipc2_Ut_unique; eassumption.
      rewrite [poly_arr _ _]lock []lock /=.

      move: /typing_normal_form_poly_absE H /H{H} /(_ (1+n+zt)) [[]].
      rewrite poly_type_norm. set f := (f in subst_poly_type f _).
      have Hf : x, f x = fold_right scons poly_var [poly_var (1 + n + zt); s] x.
      {
        rewrite /f /funcomp. case; first done.
        case; last done. by rewrite ?poly_type_norm -[RHS]ren_poly_type_id.
      }
      under ext_poly_type ? do rewrite Hf. set σ := (fold_right _ _ _).
      rewrite -?lock []lock [Ut']lock [St']lock [Pt']lock /= -?lock []lock.
      rewrite subst_poly_type_Ut' ?subst_poly_type_St' ?subst_poly_type_Pt' /σ /=.
      move [+] [].
      move /typing_normal_form_poly_arrE H /H{H} [] [+] [?].
      move /typing_normal_form_poly_arrE H /H{H} [] [+] [?].
      move /typing_normal_form_poly_arrE H /H{H} [] [+] [?].
      move /typing_normal_form_poly_arrE H /H{H} [] [] [?].

      move /(typing_weakening ( :=
        locked
        (map Ut (map ( x poly_var (x + zt)) (1+n :: xs)))
        (map St ((s, poly_var (1+zt), poly_var (1+n+zt)) :: (poly_var (1+n+zt), poly_var zt, poly_var (1+n+zt)) :: tSs))
        (map Pt ((poly_var (1+n+zt), poly_var zt, poly_var zt) :: tPs)))).
      apply: unnest.
      { move ?. rewrite /= ?app_comm_cons ?in_app_iff /=. clear. by tauto. }
      unlock. move [?] /IH. apply.
      + rewrite term_size_ren_term /=.
        rewrite [_ ]term_size_pos [_ ]term_size_pos [_ ]term_size_pos [_ ]term_size_pos. by .
      + by apply: normal_form_ren_term.
      + constructor; [| constructor]; last done.
        * exists n, 1, (1+n). constructor; first done.
          do 2 (constructor; first by apply: encodes_natI). by .
        * exists (1+n), 0, (1+n). do 3 (constructor; first by apply: encodes_natI). by .
      + constructor; last done.
        exists (1+n), 0, 0. do 3 (constructor; first by apply: encodes_natI). by .
    -
      rewrite /t_s. rewrite []lock. move /safe_poly_type_eqE [+ [ _]]. move: ts HP IH.
      do 5 (move [|?]; first done). case; last done. set σ := fold_right scons poly_var _.
      move /normal_form_many_app [_ HQs] IH _.

      rewrite [Ut']lock [St']lock /= -[locked Ut']lock -[locked St']lock ?subst_poly_type_Ut' ?subst_poly_type_St' /= -lock.
      move /copy [/Forall2_typing_Forall_iipc2 /Forall_consP [_]].
      move /Forall_consP [/iipc2_Ut_unique [ ?]]. move /Forall_consP [/iipc2_Ut_unique [ ?]].
      move /Forall_consP [/iipc2_Ut_unique [ ?]]. move /Forall_consP [/iipc2_Ut_unique [ ?]].
      move /Forall_consP [/iipc2_Ut_unique [ ?]].
      have ? := encodes_natI 1.
      move /Forall_consP [/iipc2_St_soundness {}H]. have ?: + = by apply: H; eassumption.
      move /Forall_consP [/iipc2_St_soundness {}H]. have ?: + 1 = by apply: H; eassumption.
      move /Forall_consP [/iipc2_St_soundness {}H]. have ?: + 1 = by apply: H; eassumption.
      move _ {H} /copy [/Forall2_length_eq]. move: Qs HQs IH.
      move [|]; first done. move Qs /Forall_inv IH _ /Forall2_consE [+ _].

      move: /typing_normal_form_poly_arrE H /H{H} [Q] [H1Q] [?]. set tS := (tS in St tS).
      move /(typing_weakening ( :=
         (map Ut (map ( x poly_var (x + zt)) xs)) (map St (tS :: tSs)) (map Pt tPs))).
      apply: unnest.
      { move: () ? ?. rewrite /= ?app_comm_cons ?in_app_iff /=. clear. by tauto. }
      move [?] /IH. apply.
      + rewrite term_size_ren_term /=. set P := (P in many_app P _).
        have := term_size_many_app_le P Qs. rewrite /P /=. by .
      + by apply: normal_form_ren_term.
      + constructor; last done. exists , , . do 3 (constructor; first done). by .
      + done.
    -
      rewrite /t_p. rewrite []lock. move /safe_poly_type_eqE [+ [ _]]. move: ts HP IH.
      do 5 (move [|?]; first done). case; last done. set σ := fold_right scons poly_var _.
      move /normal_form_many_app [_ HQs] IH _.

      rewrite [Ut']lock [St']lock [Pt']lock /=
        -[locked Ut']lock -[locked St']lock -[locked Pt']lock
        ?subst_poly_type_Ut' ?subst_poly_type_St' ?subst_poly_type_Pt' /= -lock.
      move /copy [/Forall2_typing_Forall_iipc2 /Forall_consP [_]].
      move /Forall_consP [/iipc2_Ut_unique [ ?]]. move /Forall_consP [/iipc2_Ut_unique [ ?]].
      move /Forall_consP [/iipc2_Ut_unique [ ?]]. move /Forall_consP [/iipc2_Ut_unique [ ?]].
      move /Forall_consP [/iipc2_Ut_unique [ ?]].
      have ? := encodes_natI 1.
      move /Forall_consP [/iipc2_Pt_soundness {}H]. have ?: * = by apply: H; eassumption.
      move /Forall_consP [/iipc2_St_soundness {}H]. have ?: + 1 = by apply: H; eassumption.
      move /Forall_consP [/iipc2_St_soundness {}H]. have ?: + = by apply: H; eassumption.
      move _ {H} /copy [/Forall2_length_eq]. move: Qs HQs IH.
      move [|]; first done. move Qs /Forall_inv IH _ /Forall2_consE [+ _].

      move: /typing_normal_form_poly_arrE H /H{H} [Q] [H1Q] [?]. set tP := (tP in Pt tP).
      move /(typing_weakening ( :=
         (map Ut (map ( x poly_var (x + zt)) xs)) (map St tSs) (map Pt (tP :: tPs)))).
      apply: unnest.
      { move: () ? ?. rewrite /= ?in_app_iff /=. clear. by tauto. }
      move [?] /IH. apply.
      + rewrite term_size_ren_term /=. set P := (P in many_app P _).
        have := term_size_many_app_le P Qs. rewrite /P /=. by .
      + by apply: normal_form_ren_term.
      + done.
      + constructor; last done. exists , , . do 3 (constructor; first done). by .
    -
      move /safe_poly_type_eqE [Hts] [] _ /Forall2_typing_Forall_iipc2.
      rewrite map_app ?[map (subst_poly_type _) (map _ _)]map_map.
      under [map _ (seq _ _)]map_ext x do rewrite Hts -rev_length subst_poly_type_Ut'.
      under [map _ h10cs]map_ext c do (rewrite subst_poly_type_h10c_poly_type; first done).
      set σ := (fold_right _ _ (rev ts)). move /Forall_appP [ Hh10cs].
      have /list_choiceHφ] : Forall ( i n, encodes_nati) n) (seq 0 δ).
      { move: /Forall_mapP. apply: Forall_impl ?. by apply: iipc2_Ut_unique. }
      exists φ c. move: Hh10cs δP Hφ /Forall_mapP /Forall_forall /Forall_forall /Forall_forall Hφ.
      move /copy [/{} + /{}]. case: c.
      + move x /iipc2_St_soundness + ? /=. move /(_x) 0 1). have : φ x + 0 = φ x by .
        apply; [done | | by apply: encodes_natI | by apply: encodes_natI].
        apply /Hφ /in_seq. by .
      + move x y z /iipc2_St_soundness + ? /=. apply; first done.
        all: apply /Hφ /in_seq; by .
      + move x y z /iipc2_Pt_soundness + ? /=. apply; first done.
        all: apply /Hφ /in_seq; by .
  }
  case /in_app_iff; first by move /in_map_iff [?] [/last_poly_var_safe_poly_type].
  case /in_app_iff; first by move /in_map_iff [[[? ?] ?]] [/last_poly_var_safe_poly_type].
  by move /in_map_iff [[[? ?] ?]] [/last_poly_var_safe_poly_type].
Qed.

End InverseTransport.

Lemma inverse_transport : SysF_INH (GammaH, poly_var tt) H10C_SAT h10cs.
Proof.
  move [M] /typing_of_type_assignment [P] [_] {M}.
  move /typing_normal_form [{}P] [/construct_h10cs_solution] H /H{H}. apply.
  - constructor. { exists 0, 0, 0. do 3 (constructor; first by apply: encodes_natI). done. }
    constructor. { exists 1, 0, 1. do 3 (constructor; first by apply: encodes_natI). done. }
    constructor. { exists 0, 1, 1. do 3 (constructor; first by apply: encodes_natI). done. }
    done.
  - constructor. { exists 0, 0, 0. do 3 (constructor; first by apply: encodes_natI). done. }
    constructor. { exists 1, 0, 0. do 3 (constructor; first by apply: encodes_natI). done. }
    done.
Qed.


Section Transport.

Variable φ : . Variable Hφ : c, In c h10cs h10c_sem c φ.

Fixpoint value_bound (cs: list h10c) : :=
  match cs with
  | [] 0
  | (h10c_one x) :: cs 1 + φ x + value_bound cs
  | (h10c_plus x y z) :: cs 1 + φ x + φ y + φ z + value_bound cs
  | (h10c_mult x y z) :: cs 1 + φ x + φ y + φ z + value_bound cs
  end.

Definition poly_num n := poly_var (n+zt).

Definition GammaU n := map ( i Ut (poly_num i)) (seq 0 (1+n)).
Definition n := map ( i St (poly_num i, poly_num 0, poly_num i)) (seq 0 (1+n)).
Definition n := map ( i St (poly_num i, poly_num 1, poly_num (1+i))) (seq 0 n).
Definition n := map ( i Pt (poly_num i, poly_num 0, poly_num 0)) (seq 0 (1+n)).

Definition GammaUSP n := locked (GammaU (S n) ( (S n) (S n)) (S n)).

Definition h10cφ_poly_type (c: h10c) : poly_type :=
  match c with
  | (h10c_one x) St (poly_num (φ x), poly_num 0, poly_num 1)
  | (h10c_plus x y z) St (poly_num (φ x), poly_num (φ y), poly_num (φ z))
  | (h10c_mult x y z) Pt (poly_num (φ x), poly_num (φ y), poly_num (φ z))
  end.

Definition φ := map h10cφ_poly_type h10cs.

Fact GammaUSn {n} : GammaU (S n) = GammaU n [Ut (poly_num (1+n))].
Proof. by rewrite /GammaU (ltac:() : 1 + S n = (S n) + 1) [seq _ (S n + 1)]seq_app map_app. Qed.

Fact GammaS0Sn {n} : (S n) = n [St (poly_num (1+n), poly_num 0, poly_num (1+n))].
Proof. by rewrite / (ltac:() : 1 + S n = (S n) + 1) [seq _ (S n + 1)]seq_app map_app. Qed.

Fact GammaS1Sn {n} : (S n) = n [St (poly_num n, poly_num 1, poly_num (1+n))].
Proof. by rewrite (ltac:() : S n = n + 1) / seq_app map_app. Qed.

Fact GammaP0Sn {n} : (S n) = n [Pt (poly_num (1+n), poly_num 0, poly_num 0)].
Proof. by rewrite / (ltac:() : 1 + S n = (S n) + 1) [seq _ (S n + 1)]seq_app map_app. Qed.

Local Arguments GammaU : simpl never.
Local Arguments : simpl never.
Local Arguments : simpl never.
Local Arguments : simpl never.

Lemma in_Ut_GammaUSP {i n} : i 1 + n In (Ut (poly_num i)) (GammaUSP n).
Proof.
  move ?. rewrite /GammaUSP -lock /GammaU.
  apply /in_app_l /in_map_iff. exists i. constructor; [done | by apply /in_seq; ].
Qed.


Lemma in_St1_GammaUSP {i n} : i n In (St (poly_num i, poly_num 1, poly_num (1+i))) (GammaUSP n).
Proof.
  move ?. rewrite /GammaUSP -lock /. apply /in_app_r /in_app_l /in_app_r.
  apply /in_map_iff. exists i. constructor; [done | by apply /in_seq; ].
Qed.


Lemma introduce_Uts (n: ) :
   ( GammaUSP n) (poly_var tt)
   GammaH (poly_var tt).
Proof.
  elim: n; first by rewrite /GammaUSP; unlock.
  move n + HSn. apply.
  apply: (iipc2_poly_varI 0 (ts := [poly_num (1+n)])); first by reflexivity.
  rewrite []lock /map subst_poly_type_Ut' [many_poly_arr]lock /=.
  move [:]. constructor.
  { abstract: . by apply /iipc2_var_InI /in_app_r /in_Ut_GammaUSP. }
  do 3 (constructor; first done). clear . constructor; last done.
  apply: (iipc2_poly_absI (S (S n) + zt)).
  - clear. have : S (S n) + zt = S (S zt) + n by . apply /Forall_appI.
    {
      rewrite -lock. do 3 (constructor; first by apply /fresh_inP).
      constructor; last done.
      rewrite /t_cs /tt. apply /fresh_in_many_poly_absI /fresh_in_many_poly_arrI; last by .
      apply /Forall_appI.
      + apply /Forall_mapP /Forall_seqP x ?. rewrite /fresh_in /= /dt /b1t /b2t /ut. by .
      + have := δP. move H. apply /Forall_mapP. apply: Forall_impl H.
        case > /=; rewrite /fresh_in /= /dt /b1t /b2t /b3t /ut /st /pt /zt /zt'; by .
    }
    rewrite /GammaUSP -lock.
    apply /Forall_appI; [| apply /Forall_appI; [apply /Forall_appI |]];
      apply /Forall_mapP /Forall_seqP; firstorder (by [|move /=; ]).
  - set σ :=in subst_poly_type σ _).
    have Hσ: x, σ x =
      (scons (poly_var 0) (scons (poly_var (S (S n) + zt)) (funcomp poly_var S))) x by move [|[|x]].
    under ext_poly_type ? do rewrite Hσ.
    have : S (S n) + zt = S (S zt) + n by .
    unlock. by firstorder by [|].
  - rewrite poly_type_norm. set σ :=in subst_poly_type σ _).
    have Hσ: x, σ x = fold_right scons poly_var [poly_var (S (S n) + zt); poly_var (S n + zt)] x by move [|[|x]].
    under ext_poly_type ? do rewrite Hσ.
    clear σ Hσ. set σ :=in subst_poly_type σ _).
    rewrite -[locked many_poly_arr]lock [Ut']lock [St']lock [Pt']lock /= -[locked Ut']lock -[locked St']lock -[locked Pt']lock
      ?subst_poly_type_Ut' ?subst_poly_type_St' ?subst_poly_type_Pt' /=.
    do 4 (apply: iipc2_poly_arrI). apply: iipc2_weakening HSn.
    clear. move t.
    rewrite /GammaUSP -?lock []lock GammaUSn GammaS0Sn GammaS1Sn GammaP0Sn.
    rewrite [GammaU]lock []lock []lock []lock /= ?in_app_iff /=. by tauto.
Qed.


Lemma introduce_Sts (n n1 n2: ) (Gamma: environment):
   + S n
   (locked GammaUSP n (St (poly_num , poly_num , poly_num (+)) :: )) (poly_var tt)
   (locked GammaUSP n ) (poly_var tt).
Proof.
  elim: [| IH] ?.
  - apply: iipc2_weakening t. rewrite ?in_app_iff /=.
    case; first by tauto. case; first by tauto. case; last by tauto.
    move . right. left. rewrite /GammaUSP -lock. apply /in_app_r /in_app_l /in_app_l.
    apply /in_map_iff. exists . have : + 0 = by .
    constructor; first done. apply /in_seq. by .
  - move H. apply: IH; first by . rewrite -[_ ]lock.
    apply: (iipc2_poly_varI 1 (ts :=
      [poly_num ( + (S )); poly_num (S ); poly_num ( + ); poly_num ; poly_num ])); first by reflexivity.
    rewrite []lock /map ?subst_poly_type_Ut' ?subst_poly_type_St'
      /(subst_poly_type _ (poly_arr _ _)) -/subst_poly_type subst_poly_type_St' /subst_poly_type /=.
    have HUSP t : In t (GammaUSP n) (locked GammaUSP n ) t.
    { move ?. apply: iipc2_var_InI. by apply /in_app_r /in_app_l. }
    constructor.
    {
      apply: iipc2_poly_arrI. apply: iipc2_weakening H ?.
      rewrite /= ?app_comm_cons ?in_app_iff /=. clear. by tauto.
    }
    do 5 (constructor; first by (apply: HUSP; apply: in_Ut_GammaUSP; by )).
    constructor.
    { apply: iipc2_var_InI. rewrite ?in_app_iff /=. by tauto. }
    constructor; first by (apply: HUSP; apply: in_St1_GammaUSP; by ).
    constructor; last done.
    have : + S = S ( + ) by . apply /HUSP /in_St1_GammaUSP. by .
Qed.


Lemma introduce_Pts (n n1 n2: ) (Gamma: environment):
   S n S n * S n
   (locked GammaUSP n (Pt (poly_num , poly_num , poly_num (*)) :: )) (poly_var tt)
   (locked GammaUSP n ) (poly_var tt).
Proof.
  elim: [| IH] ? ? ?.
  - apply: iipc2_weakening t. rewrite ?in_app_iff /=.
    case; first by tauto. case; first by tauto. case; last by tauto.
    move . right. left. rewrite /GammaUSP -lock. apply /in_app_r /in_app_r.
    apply /in_map_iff. exists . have : * 0 = 0 by .
    constructor; first done. apply /in_seq. by .
  - move H. apply: (introduce_Sts n ( * ) ); first by .
    apply: IH; [by | by | by |]. rewrite -[_ ]lock.
    apply: (iipc2_poly_varI 2 (ts :=
      [poly_num ( * (S )); poly_num (S ); poly_num ( * ); poly_num ; poly_num ])); first by reflexivity.
    rewrite []lock /map ?subst_poly_type_Ut' ?subst_poly_type_St' subst_poly_type_Pt'
      /(subst_poly_type _ (poly_arr _ _)) -/subst_poly_type subst_poly_type_Pt' /subst_poly_type /=.
    have HUSP t : In t (GammaUSP n) (locked GammaUSP n ) t.
    { move ?. apply: iipc2_var_InI. by apply /in_app_r /in_app_l. }
    constructor.
    {
      apply: iipc2_poly_arrI. apply: iipc2_weakening H ?.
      rewrite /= ?app_comm_cons ?in_app_iff /=. clear. by tauto.
    }
    do 5 (constructor; first by (apply: HUSP; apply: in_Ut_GammaUSP; by )).
    constructor.
    { apply: iipc2_var_InI. rewrite ?in_app_iff /=. by tauto. }
    constructor; first by (apply: HUSP; apply: in_St1_GammaUSP; by ).
    constructor; last done.
    have : * + = * S by . apply: iipc2_var_InI.
    rewrite ?in_app_iff /=. by tauto.
Qed.


Definition ϵ := fold_right (Nat.add) 0 (map φ (seq 0 δ)).
Lemma ϵP (x: ) : x < δ φ x ϵ.
Proof.
  suff: Forall ( x φ x ϵ) (seq 0 δ).
  { move + ? /Forall_forall. apply. apply /in_seq. by . }
  rewrite /ϵ. elim: (seq 0 δ); first by constructor.
  move {}x xs IH. constructor.
  - move /=. by .
  - apply: Forall_impl IH ? /=. by .
Qed.


Lemma introduce_φ (n: ):
  ϵ S n
   ( GammaUSP n φ) (poly_var tt)
   ( GammaUSP n) (poly_var tt).
Proof using Hφ.
  move: (Hφ). have := δP. rewrite /φ []lock + /Forall_forall + Hn.
  elim: (h10cs); first by rewrite app_nil_r.
  move [x | x y z | x y z] cs IH /Forall_consP [ /IH {}IH] /Forall_consP /= [Hφc /IH {}IH].
  - rewrite Hφc. by move /introduce_Sts /(_ ltac:()) /IH.
  - rewrite -Hφc. move /introduce_Sts H. apply /IH /H.
    have := ϵP z. by .
  - rewrite -Hφc. move /introduce_Pts H.
    apply /IH /H; [have := ϵP x | have := ϵP y | have := ϵP z]; by .
Qed.


Lemma eliminate_φ:
   ( GammaUSP (S ϵ) φ) (poly_var tt).
Proof.
  apply: (iipc2_poly_varI 3 (ts := rev (map ( x poly_num (φ x)) (seq 0 δ))));
    first by rewrite rev_length map_length seq_length.
  rewrite map_app rev_involutive. apply /Forall_appI.
  - apply /Forall_mapP /Forall_mapP /Forall_seqP x Hx.
    set ts := (map _ _). have : δ = length ts by rewrite /ts map_length seq_length.
    rewrite subst_poly_type_Ut' /subst_poly_type /ts fold_right_map_seq; first by .
    apply /iipc2_var_InI /in_app_r /in_app_l /in_Ut_GammaUSP. have := ϵP x. by .
  - apply /Forall_mapP /Forall_mapP. rewrite /φ.
    clear. have := δP. elim: (h10cs); first done.
    move c cs IH. move /Forall_consP [Hc /IH {}IH]. constructor.
    + set ts := (map _ (seq _ _)). have : δ = length ts by rewrite /ts map_length seq_length.
      move: c Hc {IH} []; rewrite /h10c_poly_type.
      * move x ?. have : δ + 1 + zt = δ + (1 + zt) by .
        rewrite subst_poly_type_St' /subst_poly_type ?fold_right_length_ts fold_right_map_seq; first by .
        apply /iipc2_var_InI /in_app_r /in_app_r. by left.
      * move x y z ?.
        rewrite subst_poly_type_St' /subst_poly_type. do 3 (rewrite fold_right_map_seq; first by ).
        apply /iipc2_var_InI /in_app_r /in_app_r. by left.
      * move x y z ?.
        rewrite subst_poly_type_Pt' /subst_poly_type. do 3 (rewrite fold_right_map_seq; first by ).
        apply /iipc2_var_InI /in_app_r /in_app_r. by left.
    + apply: Forall_impl IH ?. apply: iipc2_weakening ?.
      move: () (GammaUSP _) ? ?. clear. rewrite ?in_app_iff /=. by tauto.
Qed.

End Transport.

Lemma transport : H10C_SAT h10cs SysF_INH (GammaH, poly_var tt).
Proof.
  moveHφ]. suff: GammaH (poly_var tt).
  { move [?] /typing_to_type_assignment ?. eexists; by eassumption. }
  apply: (introduce_Uts (S (ϵ φ))).
  apply: (introduce_φ φ Hφ); first by .
  by apply: eliminate_φ.
Qed.


End H10C_SAT_to_SysF_INH.
End Argument.

Require Import Undecidability.Synthetic.Definitions.

Theorem reduction : H10C_SAT SysF_INH.
Proof.
  exists ( h10cs (Argument.GammaH h10cs, poly_var Argument.tt)).
  move h10cs. constructor.
  - exact: Argument.transport.
  - exact: Argument.inverse_transport.
Qed.