Require Import List.
Export ListNotations.
Require Import Lia.
Require Import PeanoNat.

Require Import KS_calc.
Require Import KS_exch_prelims.

Lemma ImpL_app_list_exchL : s se ps1 ps2,
  (@list_exch_L s se)
  (ImpLRule [;] s)
  ( pse1 pse2,
    (ImpLRule [;] se) *
    (@list_exch_L ) *
    (@list_exch_L )).
Proof.
intros s se exch. intro RA. inversion RA. inversion exch. subst.
inversion H. apply app2_find_hole in . destruct . repeat destruct s ; destruct p ; subst.
- destruct Γ3 ; destruct Γ4 ; destruct Γ5 ; simpl ; simpl in ; simpl in exch ; subst ; try inversion ; subst.
  + exists (Γ2 Γ1, Δ0 A :: Δ1). exists (Γ2 B :: Γ1, Δ0 Δ1). split. split ; try assumption.
    apply list_exch_L_id. apply list_exch_L_id.
  + exists (Γ2 Γ5 Γ6, Δ0 A :: Δ1). exists (Γ2 B :: Γ5 Γ6, Δ0 Δ1). split. split ; try assumption.
    apply list_exch_L_id. apply list_exch_L_id.
  + exists (Γ2 Γ4 Γ6, Δ0 A :: Δ1). exists (Γ2 B :: Γ4 Γ6, Δ0 Δ1). split. split ; try assumption.
    apply list_exch_L_id. apply list_exch_L_id.
  + exists (Γ2 ( :: Γ5) Γ4 Γ6, Δ0 A :: Δ1).
    exists (Γ2 ( :: Γ5) B :: Γ4 Γ6, Δ0 Δ1). split. split.
    assert (Γ2 ( :: Γ5) B :: Γ4 Γ6 = (Γ2 :: Γ5) B :: Γ4 Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ2 :: Γ5 A --> B :: Γ4 Γ6 = (Γ2 :: Γ5) A --> B :: Γ4 Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ2 ( :: Γ5) Γ4 Γ6 = (Γ2 :: Γ5) Γ4 Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    apply ImpLRule_I.
    assert (Γ2 Γ4 :: Γ5 Γ6 = Γ2 [] Γ4 ( :: Γ5) Γ6).
    reflexivity. rewrite . clear .
    assert (Γ2 ( :: Γ5) Γ4 Γ6 = Γ2 ( :: Γ5) Γ4 [] Γ6).
    reflexivity. rewrite . clear . apply list_exch_LI.
    assert (Γ2 B :: Γ4 :: Γ5 Γ6 = Γ2 [] (B :: Γ4) ( :: Γ5) Γ6).
    reflexivity. rewrite . clear .
    assert (Γ2 ( :: Γ5) B :: Γ4 Γ6 = Γ2 ( :: Γ5) (B :: Γ4) [] Γ6).
    reflexivity. rewrite . clear . apply list_exch_LI.
  + exists (Γ2 Γ3 Γ6, Δ0 A :: Δ1). exists (Γ2 B :: Γ3 Γ6, Δ0 Δ1). split. split ; try assumption.
    apply list_exch_L_id. apply list_exch_L_id.
  + exists (Γ2 ( :: Γ5) Γ3 Γ6, Δ0 A :: Δ1).
    exists (Γ2 ( :: Γ5) B :: Γ3 Γ6, Δ0 Δ1). split. split.
    assert (Γ2 :: Γ5 A --> B :: Γ3 Γ6 = (Γ2 :: Γ5) A --> B :: Γ3 Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ2 ( :: Γ5) B :: Γ3 Γ6 = (Γ2 :: Γ5) B :: Γ3 Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ2 ( :: Γ5) Γ3 Γ6 = (Γ2 :: Γ5) Γ3 Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    apply ImpLRule_I.
    assert (Γ2 Γ3 :: Γ5 Γ6 = Γ2 Γ3 [] ( :: Γ5) Γ6).
    reflexivity. rewrite . clear .
    assert (Γ2 ( :: Γ5) Γ3 Γ6 = Γ2 ( :: Γ5) [] Γ3 Γ6).
    reflexivity. rewrite . clear . apply list_exch_LI.
    assert (Γ2 B :: Γ3 :: Γ5 Γ6 = Γ2 (B :: Γ3) [] ( :: Γ5) Γ6).
    reflexivity. rewrite . clear .
    assert (Γ2 ( :: Γ5) B :: Γ3 Γ6 = Γ2 ( :: Γ5) [] (B :: Γ3) Γ6).
    reflexivity. rewrite . clear . apply list_exch_LI.
  + exists (Γ2 :: Γ4 Γ3 Γ6, Δ0 A :: Δ1).
    exists (Γ2 :: Γ4 B :: Γ3 Γ6, Δ0 Δ1). split. split.
    assert (Γ2 :: Γ4 A --> B :: Γ3 Γ6 = (Γ2 :: Γ4) A --> B :: Γ3 Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ2 :: Γ4 B :: Γ3 Γ6 = (Γ2 :: Γ4) B :: Γ3 Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ2 :: Γ4 Γ3 Γ6 = (Γ2 :: Γ4) Γ3 Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear . apply ImpLRule_I.
    assert (Γ2 Γ3 :: Γ4 Γ6 = Γ2 Γ3 [] ( :: Γ4) Γ6).
    reflexivity. rewrite . clear .
    assert (Γ2 :: Γ4 Γ3 Γ6 = Γ2 ( :: Γ4) [] Γ3 Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
    assert (Γ2 B :: Γ3 :: Γ4 Γ6 = Γ2 (B :: Γ3) [] ( :: Γ4) Γ6).
    reflexivity. rewrite . clear .
    assert (Γ2 :: Γ4 B :: Γ3 Γ6 = Γ2 ( :: Γ4) [] (B :: Γ3) Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
  + exists (Γ2 :: Γ5 :: Γ4 Γ3 Γ6, Δ0 A :: Δ1).
    exists (Γ2 :: Γ5 :: Γ4 B :: Γ3 Γ6, Δ0 Δ1). split. split.
    assert (Γ2 :: Γ5 :: Γ4 A --> B :: Γ3 Γ6 = (Γ2 :: Γ5 :: Γ4) A --> B :: Γ3 Γ6).
    repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ2 :: Γ5 :: Γ4 B :: Γ3 Γ6 = (Γ2 :: Γ5 :: Γ4) B :: Γ3 Γ6).
    repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ2 :: Γ5 :: Γ4 Γ3 Γ6 = (Γ2 :: Γ5 :: Γ4) Γ3 Γ6).
    repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity. rewrite . clear .
    apply ImpLRule_I.
    assert (Γ2 Γ3 :: Γ4 :: Γ5 Γ6 = Γ2 Γ3 ( :: Γ4) ( :: Γ5) Γ6).
    reflexivity. rewrite . clear .
    assert (Γ2 :: Γ5 :: Γ4 Γ3 Γ6 = Γ2 ( :: Γ5) ( :: Γ4) Γ3 Γ6).
    repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
    assert (Γ2 B :: Γ3 :: Γ4 :: Γ5 Γ6 = Γ2 (B :: Γ3) ( :: Γ4) ( :: Γ5) Γ6).
    reflexivity. rewrite . clear .
    assert (Γ2 :: Γ5 :: Γ4 B :: Γ3 Γ6 = Γ2 ( :: Γ5) ( :: Γ4) (B :: Γ3) Γ6).
    repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
- apply app2_find_hole in . destruct . repeat destruct s ; destruct p ; subst.
  + destruct Γ4 ; destruct Γ5 ; simpl ; simpl in ; simpl in exch ; subst ; try inversion ; subst.
    * rewrite app_assoc. exists ((Γ2 Γ3) Γ1, Δ0 A :: Δ1).
      exists ((Γ2 Γ3) B :: Γ1, Δ0 Δ1). split. split ; try assumption. apply list_exch_L_id.
      apply list_exch_L_id.
    * exists (Γ2 Γ5 Γ3 Γ6, Δ0 A :: Δ1).
      exists (Γ2 B :: Γ5 Γ3 Γ6, Δ0 Δ1). split. split. apply ImpLRule_I.
      assert ((Γ2 Γ3) Γ5 Γ6 = Γ2 Γ3 [] Γ5 Γ6). repeat rewrite app_assoc.
      reflexivity. rewrite . clear .
      assert (Γ2 Γ5 Γ3 Γ6 = Γ2 Γ5 [] Γ3 Γ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
      assert ((Γ2 Γ3) B :: Γ5 Γ6 = Γ2 Γ3 [] (B :: Γ5) Γ6). repeat rewrite app_assoc.
      reflexivity. rewrite . clear .
      assert (Γ2 B :: Γ5 Γ3 Γ6 = Γ2 (B :: Γ5) [] Γ3 Γ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
    * exists (Γ2 Γ4 Γ3 Γ6, Δ0 A :: Δ1).
      exists (Γ2 B :: Γ4 Γ3 Γ6, Δ0 Δ1). split. split. apply ImpLRule_I.
      assert ((Γ2 Γ3) Γ4 Γ6 = Γ2 Γ3 [] Γ4 Γ6). repeat rewrite app_assoc.
      reflexivity. rewrite . clear .
      assert (Γ2 Γ4 Γ3 Γ6 = Γ2 Γ4 [] Γ3 Γ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
      assert ((Γ2 Γ3) B :: Γ4 Γ6 = Γ2 Γ3 [] (B :: Γ4) Γ6). repeat rewrite app_assoc.
      reflexivity. rewrite . clear .
      assert (Γ2 B :: Γ4 Γ3 Γ6 = Γ2 (B :: Γ4) [] Γ3 Γ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
    * exists ((Γ2 :: Γ5) Γ4 Γ3 Γ6, Δ0 A :: Δ1).
      exists ((Γ2 :: Γ5) B :: Γ4 Γ3 Γ6, Δ0 Δ1). split. split.
      assert (Γ2 :: Γ5 A --> B :: Γ4 Γ3 Γ6 = (Γ2 :: Γ5) A --> B :: Γ4 Γ3 Γ6).
      repeat rewrite app_assoc. reflexivity. rewrite . apply ImpLRule_I.
      assert ((Γ2 Γ3) Γ4 :: Γ5 Γ6 = Γ2 Γ3 Γ4 ( :: Γ5) Γ6). repeat rewrite app_assoc.
      reflexivity. rewrite . clear .
      assert ((Γ2 :: Γ5) Γ4 Γ3 Γ6 = Γ2 ( :: Γ5) Γ4 Γ3 Γ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
      assert ((Γ2 Γ3) B :: Γ4 :: Γ5 Γ6 = Γ2 Γ3 (B :: Γ4) ( :: Γ5) Γ6). repeat rewrite app_assoc.
      reflexivity. rewrite . clear .
      assert ((Γ2 :: Γ5) B :: Γ4 Γ3 Γ6 = Γ2 ( :: Γ5) (B :: Γ4) Γ3 Γ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
  + apply app2_find_hole in . destruct . repeat destruct s ; destruct p ; subst.
    * destruct Γ5 ; simpl ; simpl in ; simpl in exch ; subst ; try inversion ; subst.
      { exists ((Γ2 Γ4 Γ3) Γ1, Δ0 A :: Δ1).
        exists ((Γ2 Γ4 Γ3) B :: Γ1, Δ0 Δ1). split. split.
        assert (Γ2 Γ4 Γ3 A --> B :: Γ1 = (Γ2 Γ4 Γ3) A --> B :: Γ1).
        repeat rewrite app_assoc. reflexivity. rewrite . apply ImpLRule_I.
        assert ((Γ2 Γ3 Γ4) Γ1 = Γ2 Γ3 [] Γ4 Γ1). repeat rewrite app_assoc.
        reflexivity. rewrite . clear .
        assert ((Γ2 Γ4 Γ3) Γ1 = Γ2 Γ4 [] Γ3 Γ1).
        repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
        assert ((Γ2 Γ3 Γ4) B :: Γ1 = Γ2 Γ3 [] Γ4 B :: Γ1). repeat rewrite app_assoc.
        reflexivity. rewrite . clear .
        assert ((Γ2 Γ4 Γ3) B :: Γ1 = Γ2 Γ4 [] Γ3 B :: Γ1).
        repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI. }
      { exists (Γ2 Γ5 Γ4 Γ3 Γ6, Δ0 A :: Δ1).
        exists (Γ2 B :: Γ5 Γ4 Γ3 Γ6, Δ0 Δ1). split. split. apply ImpLRule_I.
        repeat rewrite app_assoc. apply list_exch_LI.
        assert ((Γ2 Γ3 Γ4) B :: Γ5 Γ6 = Γ2 Γ3 Γ4 (B :: Γ5) Γ6). repeat rewrite app_assoc.
        reflexivity. rewrite . clear .
        assert (Γ2 B :: Γ5 Γ4 Γ3 Γ6 = Γ2 (B :: Γ5) Γ4 Γ3 Γ6).
        repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI. }
    * apply app2_find_hole in . destruct . repeat destruct s ; destruct p ; subst.
      { exists ((Γ2 Γ5 Γ4 Γ3) Γ1, Δ0 A :: Δ1).
        exists ((Γ2 Γ5 Γ4 Γ3) B :: Γ1, Δ0 Δ1). split. split.
        assert (Γ2 Γ5 Γ4 Γ3 A --> B :: Γ1 = (Γ2 Γ5 Γ4 Γ3) A --> B :: Γ1).
        repeat rewrite app_assoc. reflexivity. rewrite . apply ImpLRule_I.
        repeat rewrite app_assoc. apply list_exch_LI. repeat rewrite app_assoc. apply list_exch_LI. }
      { exists ((Γ2 Γ5 Γ4 Γ3 ) Γ1, Δ0 A :: Δ1).
        exists ((Γ2 Γ5 Γ4 Γ3 ) B :: Γ1, Δ0 Δ1). split. split.
        assert (Γ2 Γ5 Γ4 Γ3 A --> B :: Γ1 = (Γ2 Γ5 Γ4 Γ3 ) A --> B :: Γ1).
        repeat rewrite app_assoc. reflexivity. rewrite . apply ImpLRule_I.
        repeat rewrite app_assoc. apply list_exch_LI. repeat rewrite app_assoc. apply list_exch_LI. }
      { destruct .
        - simpl in . subst. rewrite app_nil_r.
          exists ((Γ2 x Γ4 Γ3) Γ1, Δ0 A :: Δ1).
          exists ((Γ2 x Γ4 Γ3) B :: Γ1, Δ0 Δ1). split. split.
          assert (Γ2 x Γ4 Γ3 A --> B :: Γ1 = (Γ2 x Γ4 Γ3) A --> B :: Γ1).
          repeat rewrite app_assoc. reflexivity. rewrite . clear . apply ImpLRule_I.
          repeat rewrite app_assoc. apply list_exch_LI. repeat rewrite app_assoc. apply list_exch_LI.
        - inversion . subst.
          exists ((Γ2 x) Γ4 Γ3 Γ6, Δ0 A :: Δ1).
          exists ((Γ2 x) B :: Γ4 Γ3 Γ6, Δ0 Δ1). split. split.
          assert (Γ2 (x A --> B :: ) Γ4 Γ3 Γ6 = (Γ2 x) A --> B :: Γ4 Γ3 Γ6).
          repeat rewrite app_assoc. reflexivity. rewrite . clear . apply ImpLRule_I.
          assert ((Γ2 Γ3 Γ4 x) Γ6 = Γ2 Γ3 Γ4 (x ) Γ6).
          repeat rewrite app_assoc. reflexivity. rewrite . clear .
          assert ((Γ2 x) Γ4 Γ3 Γ6 = Γ2 (x ) Γ4 Γ3 Γ6).
          repeat rewrite app_assoc. reflexivity. rewrite . clear .
          apply list_exch_LI.
          assert ((Γ2 Γ3 Γ4 x) B :: Γ6 = Γ2 Γ3 Γ4 (x B :: ) Γ6).
          repeat rewrite app_assoc. reflexivity. rewrite . clear .
          assert ((Γ2 x) B :: Γ4 Γ3 Γ6 = Γ2 (x B :: ) Γ4 Γ3 Γ6).
          repeat rewrite app_assoc. reflexivity. rewrite . clear .
          apply list_exch_LI. }
    * destruct x ; destruct Γ5 ; simpl ; simpl in ; simpl in exch ; subst ; try inversion ; subst.
      { rewrite app_nil_r. exists ((Γ2 Γ3) Γ1, Δ0 A :: Δ1).
        exists ((Γ2 Γ3) B :: Γ1, Δ0 Δ1). split. split.
        assert (Γ2 Γ3 A --> B :: Γ1 = (Γ2 Γ3) A --> B :: Γ1).
        repeat rewrite app_assoc. reflexivity. rewrite . clear . apply ImpLRule_I.
        assert ((Γ2 Γ3 ) Γ1 = Γ2 Γ3 [] Γ1).
        repeat rewrite app_assoc. reflexivity. rewrite . clear .
        assert ((Γ2 Γ3) Γ1 = Γ2 [] Γ3 Γ1).
        repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
        assert ((Γ2 Γ3 ) B :: Γ1 = Γ2 Γ3 [] B :: Γ1).
        repeat rewrite app_assoc. reflexivity. rewrite . clear .
        assert ((Γ2 Γ3) B :: Γ1 = Γ2 [] Γ3 B :: Γ1).
        repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI. }
      { rewrite app_nil_r. exists (Γ2 Γ5 Γ3 Γ6, Δ0 A :: Δ1).
        exists (Γ2 B :: Γ5 Γ3 Γ6, Δ0 Δ1). split. split.
        apply ImpLRule_I. repeat rewrite app_assoc. apply list_exch_LI.
        assert ((Γ2 Γ3 ) B :: Γ5 Γ6 = Γ2 Γ3 (B :: Γ5) Γ6).
        repeat rewrite app_assoc. reflexivity. rewrite . clear .
        assert (Γ2 B :: Γ5 Γ3 Γ6 = Γ2 (B :: Γ5) Γ3 Γ6).
        repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI. }
      { exists ((Γ2 ) x Γ3 Γ6, Δ0 A :: Δ1).
        exists ((Γ2 ) B :: x Γ3 Γ6, Δ0 Δ1). split. split.
        assert (Γ2 ( A --> B :: x) Γ3 Γ6 = (Γ2 ) A --> B :: x Γ3 Γ6).
        repeat rewrite app_assoc. reflexivity. rewrite . clear . apply ImpLRule_I.
        assert ((Γ2 Γ3 ) x Γ6 = Γ2 Γ3 [] ( x) Γ6).
        repeat rewrite app_assoc. reflexivity. rewrite . clear .
        assert ((Γ2 ) x Γ3 Γ6 = Γ2 ( x) [] Γ3 Γ6).
        repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
        assert ((Γ2 Γ3 ) B :: x Γ6 = Γ2 Γ3 [] ( B :: x) Γ6).
        repeat rewrite app_assoc. reflexivity. rewrite . clear .
        assert ((Γ2 ) B :: x Γ3 Γ6 = Γ2 ( B :: x) [] Γ3 Γ6).
        repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI. }
      { exists ((Γ2 :: Γ5 ) x Γ3 Γ6, Δ0 A :: Δ1).
        exists ((Γ2 :: Γ5 ) B :: x Γ3 Γ6, Δ0 Δ1). split. split.
        assert (Γ2 :: Γ5 ( A --> B :: x) Γ3 Γ6 = (Γ2 :: Γ5 ) A --> B :: x Γ3 Γ6).
        repeat rewrite app_assoc. simpl. repeat rewrite app_assoc.
        reflexivity. rewrite . clear . apply ImpLRule_I.
        assert ((Γ2 Γ3 ) x :: Γ5 Γ6 = Γ2 Γ3 ( x) ( :: Γ5) Γ6).
        repeat rewrite app_assoc. reflexivity. rewrite . clear .
        assert ((Γ2 :: Γ5 ) x Γ3 Γ6 = Γ2 ( :: Γ5) ( x) Γ3 Γ6).
        repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity. rewrite . clear .
        apply list_exch_LI.
        assert ((Γ2 Γ3 ) B :: x :: Γ5 Γ6 = Γ2 Γ3 ( B :: x) ( :: Γ5) Γ6).
        repeat rewrite app_assoc. reflexivity. rewrite . clear .
        assert ((Γ2 :: Γ5 ) B :: x Γ3 Γ6 = Γ2 ( :: Γ5) ( B :: x) Γ3 Γ6).
        repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity. rewrite . clear .
        apply list_exch_LI. }
  + destruct ; destruct Γ4 ; destruct Γ5 ; simpl ; simpl in ; simpl in exch ; subst ; try inversion ; subst.
    * rewrite app_nil_r. rewrite app_assoc. exists ((Γ2 x) Γ1, Δ0 A :: Δ1).
      exists ((Γ2 x) B :: Γ1, Δ0 Δ1). split. split ; try assumption. apply list_exch_L_id. apply list_exch_L_id.
    * rewrite app_nil_r. exists (Γ2 Γ5 x Γ6, Δ0 A :: Δ1).
      exists (Γ2 B :: Γ5 x Γ6, Δ0 Δ1). split. split. apply ImpLRule_I.
      assert ((Γ2 x) Γ5 Γ6 = Γ2 x [] Γ5 Γ6). repeat rewrite app_assoc.
      reflexivity. rewrite . clear .
      assert (Γ2 Γ5 x Γ6 = Γ2 Γ5 [] x Γ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
      assert ((Γ2 x) B :: Γ5 Γ6 = Γ2 x [] (B :: Γ5) Γ6). repeat rewrite app_assoc.
      reflexivity. rewrite . clear .
      assert (Γ2 B :: Γ5 x Γ6 = Γ2 (B :: Γ5) [] x Γ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
    * rewrite app_nil_r. exists (Γ2 Γ4 x Γ6, Δ0 A :: Δ1).
      exists (Γ2 B :: Γ4 x Γ6, Δ0 Δ1). split. split. apply ImpLRule_I.
      assert ((Γ2 x) Γ4 Γ6 = Γ2 x [] Γ4 Γ6). repeat rewrite app_assoc.
      reflexivity. rewrite . clear .
      assert (Γ2 Γ4 x Γ6 = Γ2 Γ4 [] x Γ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
      assert ((Γ2 x) B :: Γ4 Γ6 = Γ2 x [] (B :: Γ4) Γ6). repeat rewrite app_assoc.
      reflexivity. rewrite . clear .
      assert (Γ2 B :: Γ4 x Γ6 = Γ2 (B :: Γ4) [] x Γ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
    * rewrite app_nil_r. exists ((Γ2 :: Γ5) Γ4 x Γ6, Δ0 A :: Δ1).
      exists ((Γ2 :: Γ5) B :: Γ4 x Γ6, Δ0 Δ1). split. split.
      assert (Γ2 :: Γ5 A --> B :: Γ4 x Γ6 = (Γ2 :: Γ5) A --> B :: Γ4 x Γ6).
      repeat rewrite app_assoc. reflexivity. rewrite . apply ImpLRule_I.
      assert ((Γ2 x) Γ4 :: Γ5 Γ6 = Γ2 x Γ4 ( :: Γ5) Γ6). repeat rewrite app_assoc.
      reflexivity. rewrite . clear .
      assert ((Γ2 :: Γ5) Γ4 x Γ6 = Γ2 ( :: Γ5) Γ4 x Γ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
      assert ((Γ2 x) B :: Γ4 :: Γ5 Γ6 = Γ2 x (B :: Γ4) ( :: Γ5) Γ6). repeat rewrite app_assoc.
      reflexivity. rewrite . clear .
      assert ((Γ2 :: Γ5) B :: Γ4 x Γ6 = Γ2 ( :: Γ5) (B :: Γ4) x Γ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_LI.
    * exists ((Γ2 x) Γ6, Δ0 A :: Δ1).
      exists ((Γ2 x) B :: Γ6, Δ0 Δ1). split. split.
      assert (Γ2 (x A --> B :: ) Γ6 = (Γ2 x) A --> B :: Γ6).
      repeat rewrite app_assoc. reflexivity. rewrite . apply ImpLRule_I.
      apply list_exch_L_id. apply list_exch_L_id.
    * exists ((Γ2 :: Γ5 x) Γ6, Δ0 A :: Δ1).
      exists ((Γ2 :: Γ5 x) B :: Γ6, Δ0 Δ1). split. split.
      assert (Γ2 :: Γ5 (x A --> B :: ) Γ6 = (Γ2 :: Γ5 x) A --> B :: Γ6).
      repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity. rewrite . apply ImpLRule_I.
      assert ((Γ2 x) :: Γ5 Γ6 = Γ2 [] (x ) ( :: Γ5) Γ6). repeat rewrite app_assoc.
      reflexivity. rewrite . clear .
      assert ((Γ2 :: Γ5 x) Γ6 = Γ2 ( :: Γ5) (x ) [] Γ6).
      repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity.
      rewrite . clear . apply list_exch_LI.
      assert ((Γ2 x) B :: :: Γ5 Γ6 = Γ2 [] (x B :: ) ( :: Γ5) Γ6). repeat rewrite app_assoc.
      reflexivity. rewrite . clear .
      assert ((Γ2 :: Γ5 x) B :: Γ6 = Γ2 ( :: Γ5) (x B :: ) [] Γ6).
      repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity.
      rewrite . clear . apply list_exch_LI.
    * exists ((Γ2 :: Γ4 x) Γ6, Δ0 A :: Δ1).
      exists ((Γ2 :: Γ4 x) B :: Γ6, Δ0 Δ1). split. split.
      assert (Γ2 :: Γ4 (x A --> B :: ) Γ6 = (Γ2 :: Γ4 x) A --> B :: Γ6).
      repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity. rewrite . apply ImpLRule_I.
      assert ((Γ2 x) :: Γ4 Γ6 = Γ2 [] (x ) ( :: Γ4) Γ6). repeat rewrite app_assoc.
      reflexivity. rewrite . clear .
      assert ((Γ2 :: Γ4 x) Γ6 = Γ2 ( :: Γ4) (x ) [] Γ6).
      repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity.
      rewrite . clear . apply list_exch_LI.
      assert ((Γ2 x) B :: :: Γ4 Γ6 = Γ2 [] (x B :: ) ( :: Γ4) Γ6). repeat rewrite app_assoc.
      reflexivity. rewrite . clear .
      assert ((Γ2 :: Γ4 x) B :: Γ6 = Γ2 ( :: Γ4) (x B :: ) [] Γ6).
      repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity.
      rewrite . clear . apply list_exch_LI.
    * exists ((Γ2 :: Γ5 :: Γ4 x) Γ6, Δ0 A :: Δ1).
      exists ((Γ2 :: Γ5 :: Γ4 x) B :: Γ6, Δ0 Δ1). split. split.
      assert (Γ2 :: Γ5 :: Γ4 (x A --> B :: ) Γ6 = (Γ2 :: Γ5 :: Γ4 x) A --> B :: Γ6).
      repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. simpl.
      repeat rewrite app_assoc. reflexivity. rewrite . apply ImpLRule_I.
      assert ((Γ2 x) :: Γ4 :: Γ5 Γ6 = Γ2 (x ) ( :: Γ4) ( :: Γ5) Γ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear .
      assert ((Γ2 :: Γ5 :: Γ4 x) Γ6 = Γ2 ( :: Γ5) ( :: Γ4) (x ) Γ6).
      repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity.
      rewrite . clear . apply list_exch_LI.
      assert ((Γ2 x) B :: :: Γ4 :: Γ5 Γ6 = Γ2 (x B :: ) ( :: Γ4) ( :: Γ5) Γ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear .
      assert ((Γ2 :: Γ5 :: Γ4 x) B :: Γ6 = Γ2 ( :: Γ5) ( :: Γ4) (x B :: ) Γ6).
      repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity.
      rewrite . clear . apply list_exch_LI.
- destruct x ; destruct Γ3 ; destruct Γ4 ; destruct Γ5 ; simpl ; simpl in ; simpl in exch ;
  subst ; try inversion ; subst.
  * rewrite app_nil_r. exists (Γ0 Γ1, Δ0 A :: Δ1).
    exists (Γ0 B :: Γ1, Δ0 Δ1). split. split ; try assumption.
    apply list_exch_L_id. apply list_exch_L_id.
  * rewrite app_nil_r. exists (Γ0 Γ5 Γ6, Δ0 A :: Δ1).
    exists (Γ0 B :: Γ5 Γ6, Δ0 Δ1). split. split ; try assumption.
    apply list_exch_L_id. apply list_exch_L_id.
  * rewrite app_nil_r. exists (Γ0 Γ4 Γ6, Δ0 A :: Δ1).
    exists (Γ0 B :: Γ4 Γ6, Δ0 Δ1). split. split ; try assumption.
    apply list_exch_L_id. apply list_exch_L_id.
  * rewrite app_nil_r. exists ((Γ0 :: Γ5) Γ4 Γ6, Δ0 A :: Δ1).
    exists ((Γ0 :: Γ5) B :: Γ4 Γ6, Δ0 Δ1). split. split.
    assert (Γ0 :: Γ5 A --> B :: Γ4 Γ6 = (Γ0 :: Γ5) A --> B :: Γ4 Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . apply ImpLRule_I.
    assert (Γ0 Γ4 :: Γ5 Γ6 = Γ0 [] Γ4 ( :: Γ5) Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert ((Γ0 :: Γ5) Γ4 Γ6 = Γ0 ( :: Γ5) Γ4 [] Γ6).
    repeat rewrite app_assoc. reflexivity.
    rewrite . clear . apply list_exch_LI.
    assert (Γ0 B :: Γ4 :: Γ5 Γ6 = Γ0 [] (B :: Γ4) ( :: Γ5) Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert ((Γ0 :: Γ5) B :: Γ4 Γ6 = Γ0 ( :: Γ5) (B :: Γ4) [] Γ6).
    repeat rewrite app_assoc. reflexivity.
    rewrite . clear . apply list_exch_LI.
  * rewrite app_nil_r. exists (Γ0 Γ3 Γ6, Δ0 A :: Δ1).
    exists (Γ0 B :: Γ3 Γ6, Δ0 Δ1). split. split ; try assumption.
    apply list_exch_L_id. apply list_exch_L_id.
  * rewrite app_nil_r. exists ((Γ0 :: Γ5) Γ3 Γ6, Δ0 A :: Δ1).
    exists ((Γ0 :: Γ5) B :: Γ3 Γ6, Δ0 Δ1). split. split.
    assert (Γ0 :: Γ5 A --> B :: Γ3 Γ6 = (Γ0 :: Γ5) A --> B :: Γ3 Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . apply ImpLRule_I.
    assert (Γ0 Γ3 :: Γ5 Γ6 = Γ0 [] Γ3 ( :: Γ5) Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert ((Γ0 :: Γ5) Γ3 Γ6 = Γ0 ( :: Γ5) Γ3 [] Γ6).
    repeat rewrite app_assoc. reflexivity.
    rewrite . clear . apply list_exch_LI.
    assert (Γ0 B :: Γ3 :: Γ5 Γ6 = Γ0 [] (B :: Γ3) ( :: Γ5) Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert ((Γ0 :: Γ5) B :: Γ3 Γ6 = Γ0 ( :: Γ5) (B :: Γ3) [] Γ6).
    repeat rewrite app_assoc. reflexivity.
    rewrite . clear . apply list_exch_LI.
  * rewrite app_nil_r. exists ((Γ0 :: Γ4) Γ3 Γ6, Δ0 A :: Δ1).
    exists ((Γ0 :: Γ4) B :: Γ3 Γ6, Δ0 Δ1). split. split.
    assert (Γ0 :: Γ4 A --> B :: Γ3 Γ6 = (Γ0 :: Γ4) A --> B :: Γ3 Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . apply ImpLRule_I.
    assert ((Γ0 :: Γ4) Γ3 Γ6 = Γ0 ( :: Γ4) Γ3 [] Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ0 Γ3 :: Γ4 Γ6 = Γ0 [] Γ3 ( :: Γ4) Γ6).
    repeat rewrite app_assoc. reflexivity.
    rewrite . clear . apply list_exch_LI.
    assert ((Γ0 :: Γ4) B :: Γ3 Γ6 = Γ0 ( :: Γ4) (B :: Γ3) [] Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ0 B :: Γ3 :: Γ4 Γ6 = Γ0 [] (B :: Γ3) ( :: Γ4) Γ6).
    repeat rewrite app_assoc. reflexivity.
    rewrite . clear . apply list_exch_LI.
  * rewrite app_nil_r. exists ((Γ0 :: Γ5 :: Γ4) Γ3 Γ6, Δ0 A :: Δ1).
    exists ((Γ0 :: Γ5 :: Γ4) B :: Γ3 Γ6, Δ0 Δ1). split. split.
    assert (Γ0 :: Γ5 :: Γ4 A --> B :: Γ3 Γ6 = (Γ0 :: Γ5 :: Γ4) A --> B :: Γ3 Γ6).
    repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity. rewrite . apply ImpLRule_I.
    assert (Γ0 Γ3 :: Γ4 :: Γ5 Γ6 = Γ0 Γ3 ( :: Γ4) ( :: Γ5) Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert ((Γ0 :: Γ5 :: Γ4) Γ3 Γ6 = Γ0 ( :: Γ5) ( :: Γ4) Γ3 Γ6).
    repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity.
    rewrite . clear . apply list_exch_LI.
    assert (Γ0 B :: Γ3 :: Γ4 :: Γ5 Γ6 = Γ0 (B :: Γ3) ( :: Γ4) ( :: Γ5) Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert ((Γ0 :: Γ5 :: Γ4) B :: Γ3 Γ6 = Γ0 ( :: Γ5) ( :: Γ4) (B :: Γ3) Γ6).
    repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity.
    rewrite . clear . apply list_exch_LI.
  * exists (Γ0 x Γ6, Δ0 A :: Δ1).
    exists (Γ0 B :: x Γ6, Δ0 Δ1). split. split. repeat rewrite app_assoc. apply ImpLRule_I.
    apply list_exch_L_id. apply list_exch_L_id.
  * exists (Γ0 x :: Γ5 Γ6, Δ0 A :: Δ1).
    exists (Γ0 B :: x :: Γ5 Γ6, Δ0 Δ1). split. split. repeat rewrite app_assoc. apply ImpLRule_I.
    apply list_exch_L_id. apply list_exch_L_id.
  * exists (Γ0 x :: Γ4 Γ6, Δ0 A :: Δ1).
    exists (Γ0 B :: x :: Γ4 Γ6, Δ0 Δ1). split. split. repeat rewrite app_assoc. apply ImpLRule_I.
    apply list_exch_L_id. apply list_exch_L_id.
  * exists (Γ0 x :: Γ5 :: Γ4 Γ6, Δ0 A :: Δ1).
    exists (Γ0 B :: x :: Γ5 :: Γ4 Γ6, Δ0 Δ1). split. split.
    repeat rewrite app_assoc. apply ImpLRule_I.
    assert (Γ0 x :: Γ4 :: Γ5 Γ6 = (Γ0 x) ( :: Γ4) [] ( :: Γ5) Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ0 x :: Γ5 :: Γ4 Γ6 = (Γ0 x) ( :: Γ5) [] ( :: Γ4) Γ6).
    repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity.
    rewrite . clear . apply list_exch_LI.
    assert (Γ0 B :: x :: Γ4 :: Γ5 Γ6 = (Γ0 B :: x) ( :: Γ4) [] ( :: Γ5) Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ0 B :: x :: Γ5 :: Γ4 Γ6 = (Γ0 B :: x) ( :: Γ5) [] ( :: Γ4) Γ6).
    repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity.
    rewrite . clear . apply list_exch_LI.
  * exists (Γ0 x :: Γ3 Γ6, Δ0 A :: Δ1).
    exists (Γ0 B :: x :: Γ3 Γ6, Δ0 Δ1). split. split. repeat rewrite app_assoc. apply ImpLRule_I.
    apply list_exch_L_id. apply list_exch_L_id.
  * exists (Γ0 x :: Γ5 :: Γ3 Γ6, Δ0 A :: Δ1).
    exists (Γ0 B :: x :: Γ5 :: Γ3 Γ6, Δ0 Δ1). split. split.
    repeat rewrite app_assoc. apply ImpLRule_I.
    assert (Γ0 x :: Γ3 :: Γ5 Γ6 = (Γ0 x) ( :: Γ3) [] ( :: Γ5) Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ0 x :: Γ5 :: Γ3 Γ6 = (Γ0 x) ( :: Γ5) [] ( :: Γ3) Γ6).
    repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity.
    rewrite . clear . apply list_exch_LI.
    assert (Γ0 B :: x :: Γ3 :: Γ5 Γ6 = (Γ0 B :: x) ( :: Γ3) [] ( :: Γ5) Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ0 B :: x :: Γ5 :: Γ3 Γ6 = (Γ0 B :: x) ( :: Γ5) [] ( :: Γ3) Γ6).
    repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity.
    rewrite . clear . apply list_exch_LI.
  * exists (Γ0 x :: Γ4 :: Γ3 Γ6, Δ0 A :: Δ1).
    exists (Γ0 B :: x :: Γ4 :: Γ3 Γ6, Δ0 Δ1). split. split.
    repeat rewrite app_assoc. apply ImpLRule_I.
    assert (Γ0 x :: Γ3 :: Γ4 Γ6 = (Γ0 x) ( :: Γ3) [] ( :: Γ4) Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ0 x :: Γ4 :: Γ3 Γ6 = (Γ0 x) ( :: Γ4) [] ( :: Γ3) Γ6).
    repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity.
    rewrite . clear . apply list_exch_LI.
    assert (Γ0 B :: x :: Γ3 :: Γ4 Γ6 = (Γ0 B :: x) ( :: Γ3) [] ( :: Γ4) Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ0 B :: x :: Γ4 :: Γ3 Γ6 = (Γ0 B :: x) ( :: Γ4) [] ( :: Γ3) Γ6).
    repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity.
    rewrite . clear . apply list_exch_LI.
  * exists (Γ0 x :: Γ5 :: Γ4 :: Γ3 Γ6, Δ0 A :: Δ1).
    exists (Γ0 B :: x :: Γ5 :: Γ4 :: Γ3 Γ6, Δ0 Δ1). split. split.
    repeat rewrite app_assoc. apply ImpLRule_I.
    assert (Γ0 x :: Γ3 :: Γ4 :: Γ5 Γ6 = (Γ0 x) ( :: Γ3) ( :: Γ4) ( :: Γ5) Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ0 x :: Γ5 :: Γ4 :: Γ3 Γ6 = (Γ0 x) ( :: Γ5) ( :: Γ4) ( :: Γ3) Γ6).
    repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity.
    rewrite . clear . apply list_exch_LI.
    assert (Γ0 B :: x :: Γ3 :: Γ4 :: Γ5 Γ6 = (Γ0 B :: x) ( :: Γ3) ( :: Γ4) ( :: Γ5) Γ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Γ0 B :: x :: Γ5 :: Γ4 :: Γ3 Γ6 = (Γ0 B :: x) ( :: Γ5) ( :: Γ4) ( :: Γ3) Γ6).
    repeat rewrite app_assoc. simpl. repeat rewrite app_assoc. reflexivity.
    rewrite . clear . apply list_exch_LI.
Qed.


Lemma ImpL_app_list_exchR : s se ps1 ps2,
  (@list_exch_R s se)
  (ImpLRule [;] s)
  ( pse1 pse2,
    (ImpLRule [;] se) *
    (@list_exch_R ) *
    (@list_exch_R )).
Proof.
intros s se exch. intro RA. inversion RA. inversion exch. subst.
inversion H. apply app2_find_hole in . destruct . repeat destruct s ; destruct p ; subst.
- exists (Γ0 Γ1, Δ2 A :: Δ5 Δ4 Δ3 Δ6).
  exists (Γ0 B :: Γ1, Δ2 Δ5 Δ4 Δ3 Δ6). split. split. apply ImpLRule_I.
  assert (Δ2 A :: Δ3 Δ4 Δ5 Δ6 = (Δ2 [A]) Δ3 Δ4 Δ5 Δ6).
  rewrite app_assoc. reflexivity. rewrite . clear .
  assert (Δ2 A :: Δ5 Δ4 Δ3 Δ6 = (Δ2 [A]) Δ5 Δ4 Δ3 Δ6).
  rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_RI.
  apply list_exch_RI.
- apply app2_find_hole in . destruct . repeat destruct s ; destruct p ; subst.
  + exists (Γ0 Γ1, (Δ2 Δ5) A :: Δ4 Δ3 Δ6).
    exists (Γ0 B :: Γ1, Δ2 Δ5 Δ4 Δ3 Δ6).
    split. split.
    assert (Δ2 Δ5 Δ4 Δ3 Δ6 = (Δ2 Δ5) Δ4 Δ3 Δ6). rewrite app_assoc.
    reflexivity. rewrite . clear . apply ImpLRule_I.
    repeat rewrite app_assoc.
    assert (Δ2 Δ3 A :: Δ4 Δ5 Δ6 = Δ2 Δ3 (A :: Δ4) Δ5 Δ6).
    reflexivity. rewrite . clear .
    assert (Δ2 Δ5 A :: Δ4 Δ3 Δ6 = Δ2 Δ5 (A :: Δ4) Δ3 Δ6).
    reflexivity. rewrite . clear . apply list_exch_RI. apply list_exch_RI.
  + apply app2_find_hole in . destruct . repeat destruct s ; destruct p ; subst.
    * exists (Γ0 Γ1, (Δ2 Δ5 Δ4) A :: Δ3 Δ6).
      exists (Γ0 B :: Γ1, Δ2 Δ5 Δ4 Δ3 Δ6). split. split.
      assert (Δ2 Δ5 Δ4 Δ3 Δ6 = (Δ2 Δ5 Δ4) Δ3 Δ6). repeat rewrite app_assoc.
      reflexivity. rewrite . clear . apply ImpLRule_I. repeat rewrite app_assoc.
      assert (Δ2 Δ3 Δ4 A :: Δ5 Δ6 = Δ2 Δ3 (Δ4 [A]) Δ5 Δ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear .
      assert (Δ2 Δ5 Δ4 A :: Δ3 Δ6 = Δ2 Δ5 (Δ4 [A]) Δ3 Δ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_RI. apply list_exch_RI.
    * apply app2_find_hole in . destruct . repeat destruct s ; destruct p ; subst.
      { repeat rewrite app_assoc. exists (Γ0 Γ1, Δ2 Δ5 Δ4 Δ3 A :: Δ6).
        exists (Γ0 B :: Γ1, Δ2 Δ5 Δ4 Δ3 Δ6).
        split. split. repeat rewrite app_assoc. apply ImpLRule_I. apply list_exch_RI.
        apply list_exch_RI. }
      { repeat rewrite app_assoc. exists (Γ0 Γ1, Δ2 Δ5 Δ4 Δ3 A :: Δ1).
        exists (Γ0 B :: Γ1, Δ2 Δ5 Δ4 Δ3 Δ1). split. split. repeat rewrite app_assoc.
        apply ImpLRule_I. apply list_exch_RI. apply list_exch_RI. }
      { repeat rewrite app_assoc. exists (Γ0 Γ1, Δ2 (x A :: ) Δ4 Δ3 Δ6).
        exists (Γ0 B :: Γ1, Δ2 x Δ4 Δ3 Δ6). split. split.
        assert (Δ2 (x A :: ) Δ4 Δ3 Δ6 = (Δ2 x) A :: Δ4 Δ3 Δ6).
        repeat rewrite app_assoc. reflexivity. rewrite . clear .
        assert (Δ2 x Δ4 Δ3 Δ6 = (Δ2 x) Δ4 Δ3 Δ6).
        repeat rewrite app_assoc. reflexivity. rewrite . clear .
        apply ImpLRule_I.
        assert (Δ2 Δ3 Δ4 x A :: Δ6 = Δ2 Δ3 Δ4 (x A :: ) Δ6).
        repeat rewrite app_assoc. reflexivity. rewrite . apply list_exch_RI.
        assert (Δ2 Δ3 Δ4 x Δ6 = Δ2 Δ3 Δ4 (x ) Δ6).
        repeat rewrite app_assoc. reflexivity. rewrite . clear .
        assert (Δ2 x Δ4 Δ3 Δ6 = Δ2 (x ) Δ4 Δ3 Δ6).
        repeat rewrite app_assoc. reflexivity. rewrite . apply list_exch_RI. }
    * repeat rewrite app_assoc. exists (Γ0 Γ1, Δ2 Δ5 ( A :: x) Δ3 Δ6).
      exists (Γ0 B :: Γ1, Δ2 Δ5 ( x) Δ3 Δ6). split. split.
      assert (Δ2 Δ5 ( A :: x) Δ3 Δ6 = (Δ2 Δ5 ) A :: x Δ3 Δ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear .
      assert (Δ2 Δ5 x Δ3 Δ6 = (Δ2 Δ5 ) x Δ3 Δ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear .
      assert (Δ2 Δ5 ( x) Δ3 Δ6 = (Δ2 Δ5 ) x Δ3 Δ6).
      repeat rewrite app_assoc. reflexivity. rewrite . clear .
      apply ImpLRule_I.
      assert (Δ2 Δ3 A :: x Δ5 Δ6 = Δ2 Δ3 ( A :: x) Δ5 Δ6).
      repeat rewrite app_assoc. reflexivity. rewrite . apply list_exch_RI.
      assert (Δ2 Δ3 x Δ5 Δ6 = Δ2 Δ3 ( x) Δ5 Δ6).
      repeat rewrite app_assoc. reflexivity. rewrite . apply list_exch_RI.
  + repeat rewrite app_assoc. exists (Γ0 Γ1, Δ2 Δ5 Δ4 (x A :: ) Δ6).
    exists (Γ0 B :: Γ1, Δ2 Δ5 Δ4 (x ) Δ6). split. split.
    assert (Δ2 Δ5 Δ4 (x A :: ) Δ6 = (Δ2 Δ5 Δ4 x) A :: Δ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Δ2 Δ5 Δ4 x Δ6 = (Δ2 Δ5 Δ4 x) Δ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    assert (Δ2 Δ5 Δ4 (x ) Δ6 = (Δ2 Δ5 Δ4 x) Δ6).
    repeat rewrite app_assoc. reflexivity. rewrite . clear .
    apply ImpLRule_I.
    assert (Δ2 x A :: Δ4 Δ5 Δ6 = Δ2 (x A :: ) Δ4 Δ5 Δ6).
    repeat rewrite app_assoc. reflexivity. rewrite . apply list_exch_RI.
    assert (Δ2 x Δ4 Δ5 Δ6 = Δ2 (x ) Δ4 Δ5 Δ6).
    repeat rewrite app_assoc. reflexivity. rewrite . apply list_exch_RI.
- repeat rewrite app_assoc. exists (Γ0 Γ1, Δ0 A :: x Δ5 Δ4 Δ3 Δ6).
  exists (Γ0 B :: Γ1, Δ0 x Δ5 Δ4 Δ3 Δ6). split. split. apply ImpLRule_I.
  assert (Δ0 A :: x Δ3 Δ4 Δ5 Δ6 = (Δ0 A :: x) Δ3 Δ4 Δ5 Δ6).
  repeat rewrite app_assoc. reflexivity. rewrite . clear .
  assert (Δ0 A :: x Δ5 Δ4 Δ3 Δ6 = (Δ0 A :: x) Δ5 Δ4 Δ3 Δ6).
  repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_RI.
  assert (Δ0 x Δ3 Δ4 Δ5 Δ6 = (Δ0 x) Δ3 Δ4 Δ5 Δ6).
  repeat rewrite app_assoc. reflexivity. rewrite . clear .
  assert (Δ0 x Δ5 Δ4 Δ3 Δ6 = (Δ0 x) Δ5 Δ4 Δ3 Δ6).
  repeat rewrite app_assoc. reflexivity. rewrite . clear . apply list_exch_RI.
Qed.