Require drop_props.
Require csubst0_defs.
Require fsubst0_defs.
Require pc3_props.
Require pc3_subst0.
Require ty0_defs.
Require ty0_gen.
Require ty0_lift.
Require ty0_props.

   Section ty0_fsubst0. (****************************************************)

(*#* #stop macro *)

      Tactic Definition IH H0 v1 v2 v3 v4 v5 :=
         LApply (H0 v1 v2 v3 v4); [ Intros H_x | XEAuto ];
         LApply H_x; [ Clear H_x; Intros H_x | XEAuto ];
         LApply (H_x v5); [ Clear H_x; Intros | XEAuto ].

      Tactic Definition IHT :=
         Match Context With
            [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 ?1 ?2 c2 t2) ->
                 (wf0 ?3 c2) ->
                 (e:C) (drop i (0) ?1 (CTail e (Bind Abbr) u0)) -> ?;
              _: (subst0 ?4 ?5 ?2 ?6);
              _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
               IH H ?4 ?5 ?1 ?6 ?9.

      Tactic Definition IHTb1 :=
         Match Context With
            [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
                 (wf0 ?3 c2) ->
                 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
              _: (subst0 ?4 ?5 ?10 ?6);
              _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
               IH H '(S ?4) ?5 '(CTail ?1 (Bind ?11) ?6) ?2 ?9.

      Tactic Definition IHTb2 :=
         Match Context With
            [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
                 (wf0 ?3 c2) ->
                 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
              _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?6);
              _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
               IH H '(S ?4) ?5 '(CTail ?1 (Bind ?11) ?10) ?6 ?9.

      Tactic Definition IHC :=
         Match Context With
            [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 ?1 ?2 c2 t2) ->
                 (wf0 ?3 c2) ->
                 (e:C) (drop i (0) ?1 (CTail e (Bind Abbr) u0)) -> ?;
              _: (csubst0 ?4 ?5 ?1 ?6);
              _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
               IH H ?4 ?5 ?6 ?2 ?9.

      Tactic Definition IHCb :=
         Match Context With
            [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
                 (wf0 ?3 c2) ->
                 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
              _: (csubst0 ?4 ?5 ?1 ?6);
              _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
               IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?10) ?2 ?9.

      Tactic Definition IHTTb :=
         Match Context With
            [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
                 (wf0 ?3 c2) ->
                 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
              _: (subst0 ?4 ?5 ?10 ?6);
              _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?7);
              _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
               IH H '(S ?4) ?5 '(CTail ?1 (Bind ?11) ?6) ?7 ?9.

      Tactic Definition IHCT :=
         Match Context With
            [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 ?1 ?2 c2 t2) ->
                 (wf0 ?3 c2) ->
                 (e:C) (drop i (0) ?1 (CTail e (Bind Abbr) u0)) -> ?;
              _: (csubst0 ?4 ?5 ?1 ?6);
              _: (subst0 ?4 ?5 ?2 ?7);
              _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
               IH H ?4 ?5 ?6 ?7 ?9.

      Tactic Definition IHCTb1 :=
         Match Context With
            [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
                 (wf0 ?3 c2) ->
                 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
              _: (csubst0 ?4 ?5 ?1 ?6);
              _: (subst0 ?4 ?5 ?10 ?7);
              _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
               IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?7) ?2 ?9.

      Tactic Definition IHCTb2 :=
         Match Context With
            [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
                 (wf0 ?3 c2) ->
                 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
              _: (csubst0 ?4 ?5 ?1 ?6);
              _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?7);
              _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
               IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?10) ?7 ?9.

      Tactic Definition IHCTTb :=
         Match Context With
            [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
                 (wf0 ?3 c2) ->
                 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
              _: (csubst0 ?4 ?5 ?1 ?6);
              _: (subst0 ?4 ?5 ?10 ?7);
              _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?8);
              _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
               IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?7) ?8 ?9.

(*#* #start macro *)

(*#* #caption "substitution preserves types" *)
(*#* #cap #cap c1, c2, e, t1, t2, t #alpha u in V *)

(* NOTE: This breaks the mutual recursion between ty0_subst0 and ty0_csubst0 *)
      Theorem ty0_fsubst0: (g:?; c1:?; t1,t:?) (ty0 g c1 t1 t) ->
                           (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
                           (wf0 g c2) ->
                           (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
                           (ty0 g c2 t2 t).

(*#* #stop file *)

      Intros until 1; XElim H.
(* case 1: ty0_conv *)
      Intros until 6; XElim H4; Intros.
(* case 1.1: fsubst0_snd *)
      IHT; EApply ty0_conv; XEAuto.
(* case 1.2: fsubst0_fst *)
      IHC; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
(* case 1.3: fsubst0_both *)
      IHCT; IHCT; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
(* case 2: ty0_sort *)
      Intros until 2; XElim H0; Intros.
(* case 2.1: fsubst0_snd *)
      Subst0GenBase.
(* case 2.2: fsubst0_fst *)
      XAuto.
(* case 2.3: fsubst0_both *)
      Subst0GenBase.
(* case 3: ty0_abbr *)
      Intros until 5; XElim H3; Intros; Clear c1 c2 t t1 t2.
(* case 3.1: fsubst0_snd *)
      Subst0GenBase; Rewrite H6; Rewrite <- H3 in H5; Clear H3 H6 i t3.
      DropDis; Inversion H5; Rewrite <- H6 in H0; Rewrite H7 in H1; XEAuto.
(* case 3.2: fsubst0_fst *)
      Apply (lt_le_e n i); Intros; CSubst0Drop.
(* case 3.2.1: n < i, none *)
      EApply ty0_abbr; XEAuto.
(* case 3.2.2: n < i, csubst0_snd *)
      Inversion H0; CSubst0Drop.
      Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8;
      Clear H0 H10 H11 H12 x0 x1 x2.
      DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
      IHT; EApply ty0_abbr; XEAuto.
(* case 3.2.3: n < i, csubst0_fst *)
      Inversion H0; CSubst0Drop.
      Rewrite <- H10 in H8; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7;
      Clear H0 H10 H11 H12 x0 x1 x3.
      DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
      IHC; EApply ty0_abbr; XEAuto.
(* case 3.2.4: n < i, csubst0_both *)
      Inversion H0; CSubst0Drop.
      Rewrite <- H11 in H9; Rewrite <- H12 in H7; Rewrite <- H12 in H8; Rewrite <- H12 in H9; Rewrite <- H13 in H8;
      Clear H0 H11 H12 H13 x0 x1 x3.
      DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
      IHCT; EApply ty0_abbr; XEAuto.
(* case 3.2.5: n >= i *)
      EApply ty0_abbr; XEAuto.
(* case 3.3: fsubst0_both *)
      Subst0GenBase; Rewrite H7; Rewrite <- H3 in H4; Rewrite <- H3 in H6; Clear H3 H7 i t3.
      DropDis; Inversion H6; Rewrite <- H7 in H0; Rewrite H8 in H1.
      CSubst0Drop; XEAuto.
(* case 4: ty0_abst *)
      Intros until 5; XElim H3; Intros; Clear c1 c2 t t1 t2.
(* case 4.1: fsubst0_snd *)
      Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
(* case 4.2: fsubst0_fst *)
      Apply (lt_le_e n i); Intros; CSubst0Drop.
(* case 4.2.1: n < i, none *)
      EApply ty0_abst; XEAuto.
(* case 4.2.2: n < i, csubst0_snd *)
      Inversion H0; CSubst0Drop.
      Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8; Rewrite <- H12;
      Clear H0 H10 H11 H12 x0 x1 x2.
      DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
      IHT; EApply ty0_conv;
      [ EApply ty0_lift | EApply ty0_abst | EApply pc3_lift ]; XEAuto.
(* case 4.2.3: n < i, csubst0_fst *)
      Inversion H0; CSubst0Drop.
      Rewrite <- H10 in H8; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Rewrite <- H12;
      Clear H0 H10 H11 H12 x0 x1 x3.
      DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
      IHC; EApply ty0_abst; XEAuto.
(* case 4.2.4: n < i, csubst0_both *)
      Inversion H0; CSubst0Drop.
      Rewrite <- H11 in H9; Rewrite <- H12 in H7; Rewrite <- H12 in H8; Rewrite <- H12 in H9; Rewrite <- H13 in H8; Rewrite <- H13;
      Clear H0 H11 H12 H13 x0 x1 x3.
      DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
      IHCT; IHC; EApply ty0_conv;
      [ EApply ty0_lift | EApply ty0_abst
      | EApply pc3_lift; Try EApply pc3_fsubst0; Try Apply H0
      ]; XEAuto.
(* case 4.2.4: n >= i *)
      EApply ty0_abst; XEAuto.
(* case 4.3: fsubst0_both *)
      Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
(* case 5: ty0_bind *)
      Intros until 7; XElim H5; Intros; Clear H4.
(* case 5.1: fsubst0_snd *)
      Subst0GenBase; Rewrite H4; Clear H4 t6.
(* case 5.1.1: subst0 on left argument *)
      Ty0Correct; IHT; IHTb1; Ty0Correct.
      EApply ty0_conv;
      [ EApply ty0_bind | EApply ty0_bind | EApply pc3_fsubst0 ]; XEAuto.
(* case 5.1.2: subst0 on right argument *)
      IHTb2; Ty0Correct; EApply ty0_bind; XEAuto.
(* case 5.1.3: subst0 on both arguments *)
      Ty0Correct; IHT; IHTb1; IHTTb; Ty0Correct.
      EApply ty0_conv;
      [ EApply ty0_bind | EApply ty0_bind | EApply pc3_fsubst0 ]; XEAuto.
(* case 5.2: fsubst0_fst *)
      IHC; IHCb; Ty0Correct; EApply ty0_bind; XEAuto.
(* case 5.3: fsubst0_both *)
      Subst0GenBase; Rewrite H4; Clear H4 t6.
(* case 5.3.1: subst0 on left argument *)
      IHC; IHCb; Ty0Correct; Ty0Correct; IHCT; IHCTb1; Ty0Correct.
      EApply ty0_conv;
      [ EApply ty0_bind | EApply ty0_bind
      | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
(* case 5.3.2: subst0 on right argument *)
      IHC; IHCTb2; Ty0Correct; EApply ty0_bind; XEAuto.
(* case 5.3.3: subst0 on both arguments *)
      IHC; IHCb; Ty0Correct; Ty0Correct; IHCT; IHCTTb; Ty0Correct.
      EApply ty0_conv;
      [ EApply ty0_bind | EApply ty0_bind
      | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
(* case 6: ty0_appl *)
      Intros until 5; XElim H3; Intros.
(* case 6.1: fsubst0_snd *)
      Subst0GenBase; Rewrite H3; Clear H3 c1 c2 t t1 t2 t3.
(* case 6.1.1: subst0 on left argument *)
      Ty0Correct; Ty0GenBase; IHT; Ty0Correct.
      EApply ty0_conv;
      [ EApply ty0_appl | EApply ty0_appl | EApply pc3_fsubst0 ]; XEAuto.
(* case 6.1.2: subst0 on right argument *)
      IHT; EApply ty0_appl; XEAuto.
(* case 6.1.3: subst0 on both arguments *)
      Ty0Correct; Ty0GenBase; Move H after H10; Ty0Correct; IHT; Clear H2; IHT.
      EApply ty0_conv;
      [ EApply ty0_appl | EApply ty0_appl | EApply pc3_fsubst0 ]; XEAuto.
(* case 6.2: fsubst0_fst *)
      IHC; Clear H2; IHC; EApply ty0_appl; XEAuto.
(* case 6.3: fsubst0_both *)
      Subst0GenBase; Rewrite H3; Clear H3 c1 c2 t t1 t2 t3.
(* case 6.3.1: subst0 on left argument *)
      IHC; Ty0Correct; Ty0GenBase; Clear H2; IHC; IHCT.
      EApply ty0_conv;
      [ EApply ty0_appl | EApply ty0_appl
      | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
(* case 6.3.2: subst0 on right argument *)
      IHCT; Clear H2; IHC; EApply ty0_appl; XEAuto.
(* case 6.3.3: subst0 on both arguments *)
      IHC; Ty0Correct; Ty0GenBase; IHCT; Clear H2; IHC; Ty0Correct; IHCT.
      EApply ty0_conv;
      [ EApply ty0_appl | EApply ty0_appl
      | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
(* case 7: ty0_cast *)
      Clear c1 t t1; Intros until 5; XElim H3; Intros; Clear c2 t3.
(* case 7.1: fsubst0_snd *)
      Subst0GenBase; Rewrite H3; Clear H3 t4.
(* case 7.1.1: subst0 on left argument *)
      IHT; EApply ty0_conv;
      [ Idtac
      | EApply ty0_cast;
        [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0 ]
        | Idtac ]
      | EApply pc3_fsubst0 ]; XEAuto.
(* case 7.1.2: subst0 on right argument *)
      IHT; EApply ty0_cast; XEAuto.
(* case 7.1.3: subst0 on both arguments *)
      IHT; Clear H2; IHT.
      EApply ty0_conv;
      [ Idtac
      | EApply ty0_cast;
        [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0 ]
        | Idtac ]
      | EApply pc3_fsubst0 ]; XEAuto.
(* case 7.2: fsubst0_fst *)
      IHC; Clear H2; IHC; EApply ty0_cast; XEAuto.
(* case 6.3: fsubst0_both *)
      Subst0GenBase; Rewrite H3; Clear H3 t4.
(* case 7.3.1: subst0 on left argument *)
      IHC; IHCT; Clear H2; IHC.
      EApply ty0_conv;
      [ Idtac
      | EApply ty0_cast;
        [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]
        | Idtac ]
      | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
(* case 7.3.2: subst0 on right argument *)
      IHCT; IHC; EApply ty0_cast; XEAuto.
(* case 7.3.3: subst0 on both arguments *)
      IHC; IHCT; Clear H2; IHCT.
      EApply ty0_conv;
      [ Idtac
      | EApply ty0_cast;
        [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]
        | Idtac ]
      | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
      Qed.

      Theorem ty0_csubst0: (g:?; c1:?; t1,t2:?) (ty0 g c1 t1 t2) ->
                           (e:?; u:?; i:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
                           (c2:?) (wf0 g c2) -> (csubst0 i u c1 c2) ->
                           (ty0 g c2 t1 t2).
      Intros; EApply ty0_fsubst0; XEAuto.
      Qed.

      Theorem ty0_subst0: (g:?; c:?; t1,t:?) (ty0 g c t1 t) ->
                          (e:?; u:?; i:?) (drop i (0) c (CTail e (Bind Abbr) u)) ->
                          (t2:?) (subst0 i u t1 t2) -> (ty0 g c t2 t).
      Intros; EApply ty0_fsubst0; XEAuto.
      Qed.

   End ty0_fsubst0.

      Hints Resolve ty0_subst0 : ltlc.