Require lift_gen.
Require subst1_gen.
Require csubst1_defs.
Require pr0_lift.
Require pr0_subst1.
Require cpr0_defs.
Require pc1_props.
Require pc3_props.
Require pc3_gen.
Require ty0_defs.
Require ty0_gen.
Require ty0_lift.
Require ty0_props.
Require ty0_subst0.
Require ty0_gen_context.
Require csub0_defs.
Require csub0_props.

(*#* #caption "subject reduction" #clauses *)

(*#* #stop file *)

   Section ty0_sred_cpr0_pr0. (**********************************************)

      Tactic Definition IH H c2 t2 :=
         LApply (H c2); [ Intros H_x | XEAuto ];
         LApply H_x; [ Clear H_x; Intros H_x | XAuto ];
         LApply (H_x t2); [ Clear H_x; Intros | XEAuto ].

      Tactic Definition IH0 :=
         Match Context With
            [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
              H2: (cpr0 ?2 ?5); H3: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
               IH H1 ?5 ?3.

      Tactic Definition IH0c :=
         Match Context With
            [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
              H2: (cpr0 ?2 ?5); H3: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
               IH H1 ?5 ?3; Clear H1.

      Tactic Definition IH0B :=
         Match Context With
            [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 (CTail ?2 (Bind ?6) ?7) c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
              H2: (cpr0 ?2 ?5); H3: (ty0 ?1 (CTail ?2 (Bind ?6) ?7) ?3 ?4) |- ? ] ->
               IH H1 '(CTail ?5 (Bind ?6) ?7) ?3.

      Tactic Definition IH0Bc :=
         Match Context With
            [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 (CTail ?2 (Bind ?6) ?7) c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
              H2: (cpr0 ?2 ?5); H3: (ty0 ?1 (CTail ?2 (Bind ?6) ?7) ?3 ?4) |- ? ] ->
               IH H1 '(CTail ?5 (Bind ?6) ?7) ?3; Clear H1.

      Tactic Definition IH1 :=
         Match Context With
            [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
              H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
            IH H1 ?5 ?6.

      Tactic Definition IH1c :=
         Match Context With
            [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
              H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
            IH H1 ?5 ?6; Clear H1.

      Tactic Definition IH1Bc :=
         Match Context With
            [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 (CTail ?2 (Bind ?7) ?8) c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
              H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
            IH H1 '(CTail ?5 (Bind ?7) ?8) ?6; Clear H1.

      Tactic Definition IH1BLc :=
         Match Context With
            [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 (CTail ?2 (Bind ?7) ?8) c2)->(t2:T)(pr0 (lift ?10 ?11 ?3) t2)->(ty0 ?1 c2 t2 ?4);
              H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
            IH H1 '(CTail ?5 (Bind ?7) ?8) '(lift ?10 ?11 ?6); Clear H1.

      Tactic Definition IH1T :=
         Match Context With
            [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 (TTail ?7 ?8 ?3) t2)->(ty0 ?1 c2 t2 ?4);
              H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
            IH H1 ?5 '(TTail ?7 ?8 ?6).

      Tactic Definition IH1T2c :=
         Match Context With
            [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 (TTail ?7 ?8 ?3) t2)->(ty0 ?1 c2 t2 ?4);
              H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6); H4: (pr0 ?8 ?9) |- ? ] ->
            IH H1 ?5 '(TTail ?7 ?9 ?6); Clear H1.

      Tactic Definition IH3B :=
         Match Context With
            [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 (CTail ?2 (Bind ?7) ?8) c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
              H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6); H4: (pr0 ?8 ?9) |- ? ] ->
            IH H1 '(CTail ?5 (Bind ?7) ?9) ?6.

(*#* #start file *)

(*#* #caption "base case" *)
(*#* #cap #cap c1, c2 #alpha t1 in T, t2 in T1, t in T2 *)

      Theorem ty0_sred_cpr0_pr0: (g:?; c1:?; t1,t:?) (ty0 g c1 t1 t) ->
                                 (c2:?) (wf0 g c2) -> (cpr0 c1 c2) ->
                                 (t2:?) (pr0 t1 t2) -> (ty0 g c2 t2 t).

(*#* #stop file *)

      Intros until 1; XElim H; Intros.
(* case 1: ty0_conv *)
      IH1c; IH0c; EApply ty0_conv; XEAuto.
(* case 2: ty0_sort *)
      Inversion H2; XAuto.
(* case 3: ty0_abbr *)
      Inversion H5; Cpr0Drop; IH1c; XEAuto.
(* case 4: ty0_abst *)
      Intros; Inversion H5; Cpr0Drop; IH0; IH1.
      EApply ty0_conv;
      [ EApply ty0_lift; [ Idtac | XAuto | XEAuto ]
      | EApply ty0_abst
      | EApply pc3_lift ]; XEAuto.
(* case 5: ty0_bind *)
      Intros; Inversion H7; Clear H7.
(* case 5.1: pr0_refl *)
      IH0c; IH0Bc; IH0Bc.
      EApply ty0_bind; XEAuto.
(* case 5.2: pr0_cont *)
      IH0; IH0B; Ty0Correct; IH3B; Ty0Correct.
      EApply ty0_conv; [ EApply ty0_bind | EApply ty0_bind | Idtac ]; XEAuto.
(* case 5.3: pr0_delta *)
      Rewrite <- H8 in H1; Rewrite <- H8 in H2;
      Rewrite <- H8 in H3; Rewrite <- H8 in H4; Clear H8 b.
      IH0; IH0B; Ty0Correct; IH3B; Ty0Correct.
      EApply ty0_conv; [ EApply ty0_bind | EApply ty0_bind | Idtac ]; XEAuto.
(* case 5.4: pr0_zeta *)
      Rewrite <- H11 in H1; Rewrite <- H11 in H2; Clear H8 H9 H10 H11 b0 t2 t7 u0.
      IH0; IH1BLc; Move H3 after H8; IH0Bc; Ty0Correct; Move H8 after H4; Clear H H0 H1 H3 H6 c c1 t t1;
      NewInduction b.
(* case 5.4.1: Abbr *)
      Ty0GenContext; Subst1Gen; LiftGen; Rewrite H in H1; Clear H x0.
      EApply ty0_conv;
      [ EApply ty0_bind; XEAuto | XEAuto
      | EApply pc3_pr3_x;
        EApply (pr3_t (TTail (Bind Abbr) u (lift (1) (0) x1))); XEAuto ].
(* case 5.4.2: Abst *)
      EqFalse.
(* case 5.4.3: Void *)
      Ty0GenContext; Rewrite H0; Rewrite H0 in H2; Clear H0 t3.
      LiftGen; Rewrite <- H in H1; Clear H x0.
      EApply ty0_conv; [ EApply ty0_bind; XEAuto | XEAuto | XAuto ].
(* case 6: ty0_appl *)
      Intros; Inversion H5; Clear H5.
(* case 6.1: pr0_refl *)
      IH0c; IH0c; EApply ty0_appl; XEAuto.
(* case 6.2: pr0_cont *)
      Clear H6 H7 H8 H9 c1 k t t1 t2 t3 u1.
      IH0; Ty0Correct; Ty0GenBase; IH1c; IH0; IH1c.
      EApply ty0_conv;
      [ EApply ty0_appl; [ XEAuto | EApply ty0_bind; XEAuto ]
      | EApply ty0_appl; XEAuto
      | XEAuto ].
(* case 6.3: pr0_beta *)
      Rewrite <- H7 in H1; Rewrite <- H7 in H2; Clear H6 H7 H9 c1 t t1 t2 v v1.
      IH1T; IH0c; Ty0Correct; Ty0GenBase; IH0; IH1c.
      Move H5 after H13; Ty0GenBase; Pc3Gen; Repeat CSub0Ty0.
      EApply ty0_conv;
      [ Apply ty0_appl; [ Idtac | EApply ty0_bind ]
      | EApply ty0_bind
      | Apply (pc3_t (TTail (Bind Abbr) v2 t0))
      ]; XEAuto.
(* case 6.4: pr0_delta *)
      Rewrite <- H7 in H1; Rewrite <- H7 in H2; Clear H6 H7 H11 c1 t t1 t2 v v1.
      IH1T2c; Clear H1; Ty0Correct; NonLinear; Ty0GenBase; IH1; IH0c.
      Move H5 after H1; Ty0GenBase; Pc3Gen; Rewrite lift_bind in H0.
      Move H1 after H0; Ty0Lift b u2; Rewrite lift_bind in H17.
      Ty0GenBase.
      EApply ty0_conv;
      [ Apply ty0_appl; [ Idtac | EApply ty0_bind ]; XEAuto
      | EApply ty0_bind;
        [ Idtac
        | EApply ty0_appl; [ EApply ty0_lift | EApply ty0_conv ]
        | EApply ty0_appl; [ EApply ty0_lift | EApply ty0_bind ]
        ]; XEAuto
      | Idtac ].
      Rewrite <- lift_bind; Apply pc3_pc1;
      Apply (pc1_pr0_u2 (TTail (Flat Appl) v2 (TTail (Bind b) u2 (lift (1) (0) (TTail (Bind Abst) u t0))))); XAuto.
(* case 7: ty0_cast *)
      Intros; Inversion H5; Clear H5.
(* case 7.1: pr0_refl *)
      IH0c; IH0c; EApply ty0_cast; XEAuto.
(* case 7.2: pr0_cont *)
      Clear H6 H7 H8 H9 c1 k u1 t t1 t4 t5.
      IH0; IH1c; IH1c.
      EApply ty0_conv;
      [ XEAuto
      | EApply ty0_cast; [ EApply ty0_conv; XEAuto | XEAuto ]
      | XAuto ].
(* case 7.3: pr0_epsilon *)
      XAuto.
      Qed.

   End ty0_sred_cpr0_pr0.

   Section ty0_sred_pr3. (**********************************************)

      Theorem ty0_sred_pr1: (c:?; t1,t2:?) (pr1 t1 t2) ->
                            (g:?; t:?) (ty0 g c t1 t) ->
                            (ty0 g c t2 t).
      Intros until 1; XElim H; Intros.
(* case 1: pr1_r *)
      XAuto.
(* case 2: pr1_u *)
      EApply H1; EApply ty0_sred_cpr0_pr0; XEAuto.
      Qed.

      Theorem ty0_sred_pr2: (c:?; t1,t2:?) (pr2 c t1 t2) ->
                            (g:?; t:?) (ty0 g c t1 t) ->
                            (ty0 g c t2 t).
      Intros until 1; XElim H; Intros.
(* case 1: pr2_free *)
      EApply ty0_sred_cpr0_pr0; XEAuto.
(* case 2: pr2_u *)
      EApply ty0_subst0; Try EApply ty0_sred_cpr0_pr0; XEAuto.
      Qed.

(*#* #start file *)

(*#* #caption "general case without the reduction in the context" *)
(*#* #cap #cap c #alpha t1 in T, t2 in T1, t in T2 *)

      Theorem ty0_sred_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) ->
                            (g:?; t:?) (ty0 g c t1 t) ->
                            (ty0 g c t2 t).

(*#* #stop file *)

      Intros until 1; XElim H; Intros.
(* case 1: pr3_refl *)
      XAuto.
(* case 2: pr3_sing *)
      EApply H1; EApply ty0_sred_pr2; XEAuto.
      Qed.

   End ty0_sred_pr3.

      Tactic Definition Ty0SRed :=
         Match Context With
            | [ H1: (pr3 ?1 ?2 ?3); H2: (ty0 ?4 ?1 ?2 ?5) |- ? ] ->
               LApply (ty0_sred_pr3 ?1 ?2 ?3); [ Intros H_x | XAuto ];
               LApply (H_x ?4 ?5); [ Clear H2 H_x; Intros | XAuto ].

(*#* #start file *)

(*#* #single *)