K.KS.KS_exch_ImpL
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 : forall s se ps1 ps2,
(@list_exch_L s se) ->
(ImpLRule [ps1;ps2] s) ->
(existsT2 pse1 pse2,
(ImpLRule [pse1;pse2] se) *
(@list_exch_L ps1 pse1) *
(@list_exch_L ps2 pse2)).
Proof.
intros s se ps1 ps2 exch. intro RA. inversion RA. inversion exch. subst.
inversion H. apply app2_find_hole in H1. destruct H1. repeat destruct s ; destruct p ; subst.
- destruct Γ3 ; destruct Γ4 ; destruct Γ5 ; simpl ; simpl in e0 ; simpl in exch ; subst ; try inversion e0 ; 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 ++ (m0 :: Γ5) ++ Γ4 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ2 ++ (m0 :: Γ5) ++ B :: Γ4 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ (m0 :: Γ5) ++ B :: Γ4 ++ Γ6 = (Γ2 ++ m0 :: Γ5) ++ B :: Γ4 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m0 :: Γ5 ++ A --> B :: Γ4 ++ Γ6 = (Γ2 ++ m0 :: Γ5) ++ A --> B :: Γ4 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ (m0 :: Γ5) ++ Γ4 ++ Γ6 = (Γ2 ++ m0 :: Γ5) ++ Γ4 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply ImpLRule_I.
assert (Γ2 ++ Γ4 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ [] ++ Γ4 ++ (m0 :: Γ5) ++ Γ6).
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ (m0 :: Γ5) ++ Γ4 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ Γ4 ++ [] ++ Γ6).
reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert (Γ2 ++ B :: Γ4 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ [] ++ (B :: Γ4) ++ (m0 :: Γ5) ++ Γ6).
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ (m0 :: Γ5) ++ B :: Γ4 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ (B :: Γ4) ++ [] ++ Γ6).
reflexivity. rewrite H0. clear H0. 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 ++ (m0 :: Γ5) ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ2 ++ (m0 :: Γ5) ++ B :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m0 :: Γ5 ++ A --> B :: Γ3 ++ Γ6 = (Γ2 ++ m0 :: Γ5) ++ A --> B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ (m0 :: Γ5) ++ B :: Γ3 ++ Γ6 = (Γ2 ++ m0 :: Γ5) ++ B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ (m0 :: Γ5) ++ Γ3 ++ Γ6 = (Γ2 ++ m0 :: Γ5) ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply ImpLRule_I.
assert (Γ2 ++ Γ3 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ Γ3 ++ [] ++ (m0 :: Γ5) ++ Γ6).
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ (m0 :: Γ5) ++ Γ3 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ [] ++ Γ3 ++ Γ6).
reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert (Γ2 ++ B :: Γ3 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ (B :: Γ3) ++ [] ++ (m0 :: Γ5) ++ Γ6).
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ (m0 :: Γ5) ++ B :: Γ3 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ [] ++ (B :: Γ3) ++ Γ6).
reflexivity. rewrite H0. clear H0. apply list_exch_LI.
+ exists (Γ2 ++ m0 :: Γ4 ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ2 ++ m0 :: Γ4 ++ B :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m0 :: Γ4 ++ A --> B :: Γ3 ++ Γ6 = (Γ2 ++ m0 :: Γ4) ++ A --> B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m0 :: Γ4 ++ B :: Γ3 ++ Γ6 = (Γ2 ++ m0 :: Γ4) ++ B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m0 :: Γ4 ++ Γ3 ++ Γ6 = (Γ2 ++ m0 :: Γ4) ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert (Γ2 ++ Γ3 ++ m0 :: Γ4 ++ Γ6 = Γ2 ++ Γ3 ++ [] ++ (m0 :: Γ4) ++ Γ6).
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m0 :: Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ (m0 :: Γ4) ++ [] ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert (Γ2 ++ B :: Γ3 ++ m0 :: Γ4 ++ Γ6 = Γ2 ++ (B :: Γ3) ++ [] ++ (m0 :: Γ4) ++ Γ6).
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m0 :: Γ4 ++ B :: Γ3 ++ Γ6 = Γ2 ++ (m0 :: Γ4) ++ [] ++ (B :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
+ exists (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ B :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ A --> B :: Γ3 ++ Γ6 = (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4) ++ A --> B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ B :: Γ3 ++ Γ6 = (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4) ++ B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ Γ3 ++ Γ6 = (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4) ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply ImpLRule_I.
assert (Γ2 ++ Γ3 ++ m0 :: Γ4 ++ m1 :: Γ5 ++ Γ6 = Γ2 ++ Γ3 ++ (m0 :: Γ4) ++ (m1 :: Γ5) ++ Γ6).
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ (m1 :: Γ5) ++ (m0 :: Γ4) ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert (Γ2 ++ B :: Γ3 ++ m0 :: Γ4 ++ m1 :: Γ5 ++ Γ6 = Γ2 ++ (B :: Γ3) ++ (m0 :: Γ4) ++ (m1 :: Γ5) ++ Γ6).
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ B :: Γ3 ++ Γ6 = Γ2 ++ (m1 :: Γ5) ++ (m0 :: Γ4) ++ (B :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
- apply app2_find_hole in e0. destruct e0. repeat destruct s ; destruct p ; subst.
+ destruct Γ4 ; destruct Γ5 ; simpl ; simpl in e0 ; simpl in exch ; subst ; try inversion e0 ; 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 H0. clear H0.
assert (Γ2 ++ Γ5 ++ Γ3 ++ Γ6 = Γ2 ++ Γ5 ++ [] ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ Γ3) ++ B :: Γ5 ++ Γ6 = Γ2 ++ Γ3 ++ [] ++ (B :: Γ5) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ B :: Γ5 ++ Γ3 ++ Γ6 = Γ2 ++ (B :: Γ5) ++ [] ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. 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 H0. clear H0.
assert (Γ2 ++ Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ Γ4 ++ [] ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ Γ3) ++ B :: Γ4 ++ Γ6 = Γ2 ++ Γ3 ++ [] ++ (B :: Γ4) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ B :: Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ (B :: Γ4) ++ [] ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
* exists ((Γ2 ++ m0 :: Γ5) ++ Γ4 ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ m0 :: Γ5) ++ B :: Γ4 ++ Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m0 :: Γ5 ++ A --> B :: Γ4 ++ Γ3 ++ Γ6 = (Γ2 ++ m0 :: Γ5) ++ A --> B :: Γ4 ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert ((Γ2 ++ Γ3) ++ Γ4 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ Γ3 ++ Γ4 ++ (m0 :: Γ5) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ5) ++ Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ Γ4 ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ Γ3) ++ B :: Γ4 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ Γ3 ++ (B :: Γ4) ++ (m0 :: Γ5) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ5) ++ B :: Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ (B :: Γ4) ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
+ apply app2_find_hole in e0. destruct e0. repeat destruct s ; destruct p ; subst.
* destruct Γ5 ; simpl ; simpl in e0 ; simpl in exch ; subst ; try inversion e0 ; 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 H0. apply ImpLRule_I.
assert ((Γ2 ++ Γ3 ++ Γ4) ++ Γ1 = Γ2 ++ Γ3 ++ [] ++ Γ4 ++ Γ1). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ Γ4 ++ Γ3) ++ Γ1 = Γ2 ++ Γ4 ++ [] ++ Γ3 ++ Γ1).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ Γ3 ++ Γ4) ++ B :: Γ1 = Γ2 ++ Γ3 ++ [] ++ Γ4 ++ B :: Γ1). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ Γ4 ++ Γ3) ++ B :: Γ1 = Γ2 ++ Γ4 ++ [] ++ Γ3 ++ B :: Γ1).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. 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 H0. clear H0.
assert (Γ2 ++ B :: Γ5 ++ Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ (B :: Γ5) ++ Γ4 ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI. }
* apply app2_find_hole in e0. destruct e0. 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 H0. apply ImpLRule_I.
repeat rewrite <- app_assoc. apply list_exch_LI. repeat rewrite <- app_assoc. apply list_exch_LI. }
{ exists ((Γ2 ++ Γ5 ++ Γ4 ++ Γ3 ++ x0) ++ Γ1, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ Γ5 ++ Γ4 ++ Γ3 ++ x0) ++ B :: Γ1, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ Γ5 ++ Γ4 ++ Γ3 ++ x0 ++ A --> B :: Γ1 = (Γ2 ++ Γ5 ++ Γ4 ++ Γ3 ++ x0) ++ A --> B :: Γ1).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
repeat rewrite <- app_assoc. apply list_exch_LI. repeat rewrite <- app_assoc. apply list_exch_LI. }
{ destruct x0.
- simpl in e0. 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 H0. clear H0. apply ImpLRule_I.
repeat rewrite <- app_assoc. apply list_exch_LI. repeat rewrite <- app_assoc. apply list_exch_LI.
- inversion e0. subst.
exists ((Γ2 ++ x) ++ x0 ++ Γ4 ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ x) ++ B :: x0 ++ Γ4 ++ Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ (x ++ A --> B :: x0) ++ Γ4 ++ Γ3 ++ Γ6 = (Γ2 ++ x) ++ A --> B :: x0 ++ Γ4 ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert ((Γ2 ++ Γ3 ++ Γ4 ++ x) ++ x0 ++ Γ6 = Γ2 ++ Γ3 ++ Γ4 ++ (x ++ x0) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ x) ++ x0 ++ Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ (x ++ x0) ++ Γ4 ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply list_exch_LI.
assert ((Γ2 ++ Γ3 ++ Γ4 ++ x) ++ B :: x0 ++ Γ6 = Γ2 ++ Γ3 ++ Γ4 ++ (x ++ B :: x0) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ x) ++ B :: x0 ++ Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ (x ++ B :: x0) ++ Γ4 ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply list_exch_LI. }
* destruct x ; destruct Γ5 ; simpl ; simpl in e0 ; simpl in exch ; subst ; try inversion e0 ; subst.
{ rewrite app_nil_r. exists ((Γ2 ++ x0 ++ Γ3) ++ Γ1, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ x0 ++ Γ3) ++ B :: Γ1, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ x0 ++ Γ3 ++ A --> B :: Γ1 = (Γ2 ++ x0 ++ Γ3) ++ A --> B :: Γ1).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert ((Γ2 ++ Γ3 ++ x0) ++ Γ1 = Γ2 ++ Γ3 ++ [] ++ x0 ++ Γ1).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ x0 ++ Γ3) ++ Γ1 = Γ2 ++ x0 ++ [] ++ Γ3 ++ Γ1).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ Γ3 ++ x0) ++ B :: Γ1 = Γ2 ++ Γ3 ++ [] ++ x0 ++ B :: Γ1).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ x0 ++ Γ3) ++ B :: Γ1 = Γ2 ++ x0 ++ [] ++ Γ3 ++ B :: Γ1).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI. }
{ rewrite app_nil_r. exists (Γ2 ++ Γ5 ++ x0 ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ2 ++ B :: Γ5 ++ x0 ++ Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
apply ImpLRule_I. repeat rewrite <- app_assoc. apply list_exch_LI.
assert ((Γ2 ++ Γ3 ++ x0) ++ B :: Γ5 ++ Γ6 = Γ2 ++ Γ3 ++ x0 ++ (B :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ B :: Γ5 ++ x0 ++ Γ3 ++ Γ6 = Γ2 ++ (B :: Γ5) ++ x0 ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI. }
{ exists ((Γ2 ++ x0) ++ x ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ x0) ++ B :: x ++ Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ (x0 ++ A --> B :: x) ++ Γ3 ++ Γ6 = (Γ2 ++ x0) ++ A --> B :: x ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert ((Γ2 ++ Γ3 ++ x0) ++ x ++ Γ6 = Γ2 ++ Γ3 ++ [] ++ (x0 ++ x) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ x0) ++ x ++ Γ3 ++ Γ6 = Γ2 ++ (x0 ++ x) ++ [] ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ Γ3 ++ x0) ++ B :: x ++ Γ6 = Γ2 ++ Γ3 ++ [] ++ (x0 ++ B :: x) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ x0) ++ B :: x ++ Γ3 ++ Γ6 = Γ2 ++ (x0 ++ B :: x) ++ [] ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI. }
{ exists ((Γ2 ++ m0 :: Γ5 ++ x0) ++ x ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ m0 :: Γ5 ++ x0) ++ B :: x ++ Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m0 :: Γ5 ++ (x0 ++ A --> B :: x) ++ Γ3 ++ Γ6 = (Γ2 ++ m0 :: Γ5 ++ x0) ++ A --> B :: x ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert ((Γ2 ++ Γ3 ++ x0) ++ x ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ Γ3 ++ (x0 ++ x) ++ (m0 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ5 ++ x0) ++ x ++ Γ3 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ (x0 ++ x) ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply list_exch_LI.
assert ((Γ2 ++ Γ3 ++ x0) ++ B :: x ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ Γ3 ++ (x0 ++ B :: x) ++ (m0 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ5 ++ x0) ++ B :: x ++ Γ3 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ (x0 ++ B :: x) ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply list_exch_LI. }
+ destruct x0 ; destruct Γ4 ; destruct Γ5 ; simpl ; simpl in e0 ; simpl in exch ; subst ; try inversion e0 ; 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 H0. clear H0.
assert (Γ2 ++ Γ5 ++ x ++ Γ6 = Γ2 ++ Γ5 ++ [] ++ x ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ x) ++ B :: Γ5 ++ Γ6 = Γ2 ++ x ++ [] ++ (B :: Γ5) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ B :: Γ5 ++ x ++ Γ6 = Γ2 ++ (B :: Γ5) ++ [] ++ x ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. 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 H0. clear H0.
assert (Γ2 ++ Γ4 ++ x ++ Γ6 = Γ2 ++ Γ4 ++ [] ++ x ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ x) ++ B :: Γ4 ++ Γ6 = Γ2 ++ x ++ [] ++ (B :: Γ4) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ B :: Γ4 ++ x ++ Γ6 = Γ2 ++ (B :: Γ4) ++ [] ++ x ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
* rewrite app_nil_r. exists ((Γ2 ++ m0 :: Γ5) ++ Γ4 ++ x ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ m0 :: Γ5) ++ B :: Γ4 ++ x ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m0 :: Γ5 ++ A --> B :: Γ4 ++ x ++ Γ6 = (Γ2 ++ m0 :: Γ5) ++ A --> B :: Γ4 ++ x ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert ((Γ2 ++ x) ++ Γ4 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ x ++ Γ4 ++ (m0 :: Γ5) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ5) ++ Γ4 ++ x ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ Γ4 ++ x ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ x) ++ B :: Γ4 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ x ++ (B :: Γ4) ++ (m0 :: Γ5) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ5) ++ B :: Γ4 ++ x ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ (B :: Γ4) ++ x ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
* exists ((Γ2 ++ x) ++ x0 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ x) ++ B :: x0 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ (x ++ A --> B :: x0) ++ Γ6 = (Γ2 ++ x) ++ A --> B :: x0 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
apply list_exch_L_id. apply list_exch_L_id.
* exists ((Γ2 ++ m0 :: Γ5 ++ x) ++ x0 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ m0 :: Γ5 ++ x) ++ B :: x0 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m0 :: Γ5 ++ (x ++ A --> B :: x0) ++ Γ6 = (Γ2 ++ m0 :: Γ5 ++ x) ++ A --> B :: x0 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert ((Γ2 ++ x) ++ x0 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ [] ++ (x ++ x0) ++ (m0 :: Γ5) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ5 ++ x) ++ x0 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ (x ++ x0) ++ [] ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ x) ++ B :: x0 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ [] ++ (x ++ B :: x0) ++ (m0 :: Γ5) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ5 ++ x) ++ B :: x0 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ (x ++ B :: x0) ++ [] ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
* exists ((Γ2 ++ m0 :: Γ4 ++ x) ++ x0 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ m0 :: Γ4 ++ x) ++ B :: x0 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m0 :: Γ4 ++ (x ++ A --> B :: x0) ++ Γ6 = (Γ2 ++ m0 :: Γ4 ++ x) ++ A --> B :: x0 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert ((Γ2 ++ x) ++ x0 ++ m0 :: Γ4 ++ Γ6 = Γ2 ++ [] ++ (x ++ x0) ++ (m0 :: Γ4) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ4 ++ x) ++ x0 ++ Γ6 = Γ2 ++ (m0 :: Γ4) ++ (x ++ x0) ++ [] ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ x) ++ B :: x0 ++ m0 :: Γ4 ++ Γ6 = Γ2 ++ [] ++ (x ++ B :: x0) ++ (m0 :: Γ4) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ4 ++ x) ++ B :: x0 ++ Γ6 = Γ2 ++ (m0 :: Γ4) ++ (x ++ B :: x0) ++ [] ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
* exists ((Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ x) ++ x0 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ x) ++ B :: x0 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ (x ++ A --> B :: x0) ++ Γ6 = (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ x) ++ A --> B :: x0 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. simpl.
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert ((Γ2 ++ x) ++ x0 ++ m0 :: Γ4 ++ m1 :: Γ5 ++ Γ6 = Γ2 ++ (x ++ x0) ++ (m0 :: Γ4) ++ (m1 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ x) ++ x0 ++ Γ6 = Γ2 ++ (m1 :: Γ5) ++ (m0 :: Γ4) ++ (x ++ x0) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ x) ++ B :: x0 ++ m0 :: Γ4 ++ m1 :: Γ5 ++ Γ6 = Γ2 ++ (x ++ B :: x0) ++ (m0 :: Γ4) ++ (m1 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ x) ++ B :: x0 ++ Γ6 = Γ2 ++ (m1 :: Γ5) ++ (m0 :: Γ4) ++ (x ++ B :: x0) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
- destruct x ; destruct Γ3 ; destruct Γ4 ; destruct Γ5 ; simpl ; simpl in e0 ; simpl in exch ;
subst ; try inversion e0 ; 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 ++ m0 :: Γ5) ++ Γ4 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ0 ++ m0 :: Γ5) ++ B :: Γ4 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ0 ++ m0 :: Γ5 ++ A --> B :: Γ4 ++ Γ6 = (Γ0 ++ m0 :: Γ5) ++ A --> B :: Γ4 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert (Γ0 ++ Γ4 ++ m0 :: Γ5 ++ Γ6 = Γ0 ++ [] ++ Γ4 ++ (m0 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ0 ++ m0 :: Γ5) ++ Γ4 ++ Γ6 = Γ0 ++ (m0 :: Γ5) ++ Γ4 ++ [] ++ Γ6).
repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert (Γ0 ++ B :: Γ4 ++ m0 :: Γ5 ++ Γ6 = Γ0 ++ [] ++ (B :: Γ4) ++ (m0 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ0 ++ m0 :: Γ5) ++ B :: Γ4 ++ Γ6 = Γ0 ++ (m0 :: Γ5) ++ (B :: Γ4) ++ [] ++ Γ6).
repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. 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 ++ m0 :: Γ5) ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ0 ++ m0 :: Γ5) ++ B :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ0 ++ m0 :: Γ5 ++ A --> B :: Γ3 ++ Γ6 = (Γ0 ++ m0 :: Γ5) ++ A --> B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert (Γ0 ++ Γ3 ++ m0 :: Γ5 ++ Γ6 = Γ0 ++ [] ++ Γ3 ++ (m0 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ0 ++ m0 :: Γ5) ++ Γ3 ++ Γ6 = Γ0 ++ (m0 :: Γ5) ++ Γ3 ++ [] ++ Γ6).
repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert (Γ0 ++ B :: Γ3 ++ m0 :: Γ5 ++ Γ6 = Γ0 ++ [] ++ (B :: Γ3) ++ (m0 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ0 ++ m0 :: Γ5) ++ B :: Γ3 ++ Γ6 = Γ0 ++ (m0 :: Γ5) ++ (B :: Γ3) ++ [] ++ Γ6).
repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
* rewrite app_nil_r. exists ((Γ0 ++ m0 :: Γ4) ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ0 ++ m0 :: Γ4) ++ B :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ0 ++ m0 :: Γ4 ++ A --> B :: Γ3 ++ Γ6 = (Γ0 ++ m0 :: Γ4) ++ A --> B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert ((Γ0 ++ m0 :: Γ4) ++ Γ3 ++ Γ6 = Γ0 ++ (m0 :: Γ4) ++ Γ3 ++ [] ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ Γ3 ++ m0 :: Γ4 ++ Γ6 = Γ0 ++ [] ++ Γ3 ++ (m0 :: Γ4) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ0 ++ m0 :: Γ4) ++ B :: Γ3 ++ Γ6 = Γ0 ++ (m0 :: Γ4) ++ (B :: Γ3) ++ [] ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ B :: Γ3 ++ m0 :: Γ4 ++ Γ6 = Γ0 ++ [] ++ (B :: Γ3) ++ (m0 :: Γ4) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
* rewrite app_nil_r. exists ((Γ0 ++ m1 :: Γ5 ++ m0 :: Γ4) ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ0 ++ m1 :: Γ5 ++ m0 :: Γ4) ++ B :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ0 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ A --> B :: Γ3 ++ Γ6 = (Γ0 ++ m1 :: Γ5 ++ m0 :: Γ4) ++ A --> B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert (Γ0 ++ Γ3 ++ m0 :: Γ4 ++ m1 :: Γ5 ++ Γ6 = Γ0 ++ Γ3 ++ (m0 :: Γ4) ++ (m1 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ0 ++ m1 :: Γ5 ++ m0 :: Γ4) ++ Γ3 ++ Γ6 = Γ0 ++ (m1 :: Γ5) ++ (m0 :: Γ4) ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert (Γ0 ++ B :: Γ3 ++ m0 :: Γ4 ++ m1 :: Γ5 ++ Γ6 = Γ0 ++ (B :: Γ3) ++ (m0 :: Γ4) ++ (m1 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ0 ++ m1 :: Γ5 ++ m0 :: Γ4) ++ B :: Γ3 ++ Γ6 = Γ0 ++ (m1 :: Γ5) ++ (m0 :: Γ4) ++ (B :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. 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 ++ m0 :: Γ5 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ0 ++ B :: x ++ m0 :: Γ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 ++ m0 :: Γ4 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ0 ++ B :: x ++ m0 :: Γ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 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ0 ++ B :: x ++ m1 :: Γ5 ++ m0 :: Γ4 ++ Γ6, Δ0 ++ Δ1). split. split.
repeat rewrite <- app_assoc. apply ImpLRule_I.
assert (Γ0 ++ x ++ m0 :: Γ4 ++ m1 :: Γ5 ++ Γ6 = (Γ0 ++ x) ++ (m0 :: Γ4) ++ [] ++ (m1 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ x ++ m1 :: Γ5 ++ m0 :: Γ4 ++ Γ6 = (Γ0 ++ x) ++ (m1 :: Γ5) ++ [] ++ (m0 :: Γ4) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert (Γ0 ++ B :: x ++ m0 :: Γ4 ++ m1 :: Γ5 ++ Γ6 = (Γ0 ++ B :: x) ++ (m0 :: Γ4) ++ [] ++ (m1 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ B :: x ++ m1 :: Γ5 ++ m0 :: Γ4 ++ Γ6 = (Γ0 ++ B :: x) ++ (m1 :: Γ5) ++ [] ++ (m0 :: Γ4) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
* exists (Γ0 ++ x ++ m0 :: Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ0 ++ B :: x ++ m0 :: Γ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 ++ m1 :: Γ5 ++ m0 :: Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ0 ++ B :: x ++ m1 :: Γ5 ++ m0 :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
repeat rewrite <- app_assoc. apply ImpLRule_I.
assert (Γ0 ++ x ++ m0 :: Γ3 ++ m1 :: Γ5 ++ Γ6 = (Γ0 ++ x) ++ (m0 :: Γ3) ++ [] ++ (m1 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ x ++ m1 :: Γ5 ++ m0 :: Γ3 ++ Γ6 = (Γ0 ++ x) ++ (m1 :: Γ5) ++ [] ++ (m0 :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert (Γ0 ++ B :: x ++ m0 :: Γ3 ++ m1 :: Γ5 ++ Γ6 = (Γ0 ++ B :: x) ++ (m0 :: Γ3) ++ [] ++ (m1 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ B :: x ++ m1 :: Γ5 ++ m0 :: Γ3 ++ Γ6 = (Γ0 ++ B :: x) ++ (m1 :: Γ5) ++ [] ++ (m0 :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
* exists (Γ0 ++ x ++ m1 :: Γ4 ++ m0 :: Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ0 ++ B :: x ++ m1 :: Γ4 ++ m0 :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
repeat rewrite <- app_assoc. apply ImpLRule_I.
assert (Γ0 ++ x ++ m0 :: Γ3 ++ m1 :: Γ4 ++ Γ6 = (Γ0 ++ x) ++ (m0 :: Γ3) ++ [] ++ (m1 :: Γ4) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ x ++ m1 :: Γ4 ++ m0 :: Γ3 ++ Γ6 = (Γ0 ++ x) ++ (m1 :: Γ4) ++ [] ++ (m0 :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert (Γ0 ++ B :: x ++ m0 :: Γ3 ++ m1 :: Γ4 ++ Γ6 = (Γ0 ++ B :: x) ++ (m0 :: Γ3) ++ [] ++ (m1 :: Γ4) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ B :: x ++ m1 :: Γ4 ++ m0 :: Γ3 ++ Γ6 = (Γ0 ++ B :: x) ++ (m1 :: Γ4) ++ [] ++ (m0 :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
* exists (Γ0 ++ x ++ m2 :: Γ5 ++ m1 :: Γ4 ++ m0 :: Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ0 ++ B :: x ++ m2 :: Γ5 ++ m1 :: Γ4 ++ m0 :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
repeat rewrite <- app_assoc. apply ImpLRule_I.
assert (Γ0 ++ x ++ m0 :: Γ3 ++ m1 :: Γ4 ++ m2 :: Γ5 ++ Γ6 = (Γ0 ++ x) ++ (m0 :: Γ3) ++ (m1 :: Γ4) ++ (m2 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ x ++ m2 :: Γ5 ++ m1 :: Γ4 ++ m0 :: Γ3 ++ Γ6 = (Γ0 ++ x) ++ (m2 :: Γ5) ++ (m1 :: Γ4) ++ (m0 :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert (Γ0 ++ B :: x ++ m0 :: Γ3 ++ m1 :: Γ4 ++ m2 :: Γ5 ++ Γ6 = (Γ0 ++ B :: x) ++ (m0 :: Γ3) ++ (m1 :: Γ4) ++ (m2 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ B :: x ++ m2 :: Γ5 ++ m1 :: Γ4 ++ m0 :: Γ3 ++ Γ6 = (Γ0 ++ B :: x) ++ (m2 :: Γ5) ++ (m1 :: Γ4) ++ (m0 :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
Qed.
Lemma ImpL_app_list_exchR : forall s se ps1 ps2,
(@list_exch_R s se) ->
(ImpLRule [ps1;ps2] s) ->
(existsT2 pse1 pse2,
(ImpLRule [pse1;pse2] se) *
(@list_exch_R ps1 pse1) *
(@list_exch_R ps2 pse2)).
Proof.
intros s se ps1 ps2 exch. intro RA. inversion RA. inversion exch. subst.
inversion H. apply app2_find_hole in H2. destruct H2. 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 H0. clear H0.
assert (Δ2 ++ A :: Δ5 ++ Δ4 ++ Δ3 ++ Δ6 = (Δ2 ++ [A]) ++ Δ5 ++ Δ4 ++ Δ3 ++ Δ6).
rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_RI.
apply list_exch_RI.
- apply app2_find_hole in e0. destruct e0. 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 H0. clear H0. apply ImpLRule_I.
repeat rewrite <- app_assoc.
assert (Δ2 ++ Δ3 ++ A :: Δ4 ++ Δ5 ++ Δ6 = Δ2 ++ Δ3 ++ (A :: Δ4) ++ Δ5 ++ Δ6).
reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ Δ5 ++ A :: Δ4 ++ Δ3 ++ Δ6 = Δ2 ++ Δ5 ++ (A :: Δ4) ++ Δ3 ++ Δ6).
reflexivity. rewrite H0. clear H0. apply list_exch_RI. apply list_exch_RI.
+ apply app2_find_hole in e0. destruct e0. 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 H0. clear H0. 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 H0. clear H0.
assert (Δ2 ++ Δ5 ++ Δ4 ++ A :: Δ3 ++ Δ6 = Δ2 ++ Δ5 ++ (Δ4 ++ [A]) ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_RI. apply list_exch_RI.
* apply app2_find_hole in e0. destruct e0. 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 ++ x0 ++ A :: Δ1).
exists (Γ0 ++ B :: Γ1, Δ2 ++ Δ5 ++ Δ4 ++ Δ3 ++ x0 ++ Δ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 :: x0) ++ Δ4 ++ Δ3 ++ Δ6).
exists (Γ0 ++ B :: Γ1, Δ2 ++ x ++ x0 ++ Δ4 ++ Δ3 ++ Δ6). split. split.
assert (Δ2 ++ (x ++ A :: x0) ++ Δ4 ++ Δ3 ++ Δ6 = (Δ2 ++ x) ++ A :: x0 ++ Δ4 ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ x ++ x0 ++ Δ4 ++ Δ3 ++ Δ6 = (Δ2 ++ x) ++ x0 ++ Δ4 ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply ImpLRule_I.
assert (Δ2 ++ Δ3 ++ Δ4 ++ x ++ A :: x0 ++ Δ6 = Δ2 ++ Δ3 ++ Δ4 ++ (x ++ A :: x0) ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply list_exch_RI.
assert (Δ2 ++ Δ3 ++ Δ4 ++ x ++ x0 ++ Δ6 = Δ2 ++ Δ3 ++ Δ4 ++ (x ++ x0) ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ x ++ x0 ++ Δ4 ++ Δ3 ++ Δ6 = Δ2 ++ (x ++ x0) ++ Δ4 ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply list_exch_RI. }
* repeat rewrite <- app_assoc. exists (Γ0 ++ Γ1, Δ2 ++ Δ5 ++ (x0 ++ A :: x) ++ Δ3 ++ Δ6).
exists (Γ0 ++ B :: Γ1, Δ2 ++ Δ5 ++ (x0 ++ x) ++ Δ3 ++ Δ6). split. split.
assert (Δ2 ++ Δ5 ++ (x0 ++ A :: x) ++ Δ3 ++ Δ6 = (Δ2 ++ Δ5 ++ x0) ++ A :: x ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ Δ5 ++ x0 ++ x ++ Δ3 ++ Δ6 = (Δ2 ++ Δ5 ++ x0) ++ x ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ Δ5 ++ (x0 ++ x) ++ Δ3 ++ Δ6 = (Δ2 ++ Δ5 ++ x0) ++ x ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply ImpLRule_I.
assert (Δ2 ++ Δ3 ++ x0 ++ A :: x ++ Δ5 ++ Δ6 = Δ2 ++ Δ3 ++ (x0 ++ A :: x) ++ Δ5 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply list_exch_RI.
assert (Δ2 ++ Δ3 ++ x0 ++ x ++ Δ5 ++ Δ6 = Δ2 ++ Δ3 ++ (x0 ++ x) ++ Δ5 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply list_exch_RI.
+ repeat rewrite <- app_assoc. exists (Γ0 ++ Γ1, Δ2 ++ Δ5 ++ Δ4 ++ (x ++ A :: x0) ++ Δ6).
exists (Γ0 ++ B :: Γ1, Δ2 ++ Δ5 ++ Δ4 ++ (x ++ x0) ++ Δ6). split. split.
assert (Δ2 ++ Δ5 ++ Δ4 ++ (x ++ A :: x0) ++ Δ6 = (Δ2 ++ Δ5 ++ Δ4 ++ x) ++ A :: x0 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ Δ5 ++ Δ4 ++ x ++ x0 ++ Δ6 = (Δ2 ++ Δ5 ++ Δ4 ++ x) ++ x0 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ Δ5 ++ Δ4 ++ (x ++ x0) ++ Δ6 = (Δ2 ++ Δ5 ++ Δ4 ++ x) ++ x0 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply ImpLRule_I.
assert (Δ2 ++ x ++ A :: x0 ++ Δ4 ++ Δ5 ++ Δ6 = Δ2 ++ (x ++ A :: x0) ++ Δ4 ++ Δ5 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply list_exch_RI.
assert (Δ2 ++ x ++ x0 ++ Δ4 ++ Δ5 ++ Δ6 = Δ2 ++ (x ++ x0) ++ Δ4 ++ Δ5 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. 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 H0. clear H0.
assert (Δ0 ++ A :: x ++ Δ5 ++ Δ4 ++ Δ3 ++ Δ6 = (Δ0 ++ A :: x) ++ Δ5 ++ Δ4 ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_RI.
assert (Δ0 ++ x ++ Δ3 ++ Δ4 ++ Δ5 ++ Δ6 = (Δ0 ++ x) ++ Δ3 ++ Δ4 ++ Δ5 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Δ0 ++ x ++ Δ5 ++ Δ4 ++ Δ3 ++ Δ6 = (Δ0 ++ x) ++ Δ5 ++ Δ4 ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_RI.
Qed.
Export ListNotations.
Require Import Lia.
Require Import PeanoNat.
Require Import KS_calc.
Require Import KS_exch_prelims.
Lemma ImpL_app_list_exchL : forall s se ps1 ps2,
(@list_exch_L s se) ->
(ImpLRule [ps1;ps2] s) ->
(existsT2 pse1 pse2,
(ImpLRule [pse1;pse2] se) *
(@list_exch_L ps1 pse1) *
(@list_exch_L ps2 pse2)).
Proof.
intros s se ps1 ps2 exch. intro RA. inversion RA. inversion exch. subst.
inversion H. apply app2_find_hole in H1. destruct H1. repeat destruct s ; destruct p ; subst.
- destruct Γ3 ; destruct Γ4 ; destruct Γ5 ; simpl ; simpl in e0 ; simpl in exch ; subst ; try inversion e0 ; 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 ++ (m0 :: Γ5) ++ Γ4 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ2 ++ (m0 :: Γ5) ++ B :: Γ4 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ (m0 :: Γ5) ++ B :: Γ4 ++ Γ6 = (Γ2 ++ m0 :: Γ5) ++ B :: Γ4 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m0 :: Γ5 ++ A --> B :: Γ4 ++ Γ6 = (Γ2 ++ m0 :: Γ5) ++ A --> B :: Γ4 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ (m0 :: Γ5) ++ Γ4 ++ Γ6 = (Γ2 ++ m0 :: Γ5) ++ Γ4 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply ImpLRule_I.
assert (Γ2 ++ Γ4 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ [] ++ Γ4 ++ (m0 :: Γ5) ++ Γ6).
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ (m0 :: Γ5) ++ Γ4 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ Γ4 ++ [] ++ Γ6).
reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert (Γ2 ++ B :: Γ4 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ [] ++ (B :: Γ4) ++ (m0 :: Γ5) ++ Γ6).
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ (m0 :: Γ5) ++ B :: Γ4 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ (B :: Γ4) ++ [] ++ Γ6).
reflexivity. rewrite H0. clear H0. 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 ++ (m0 :: Γ5) ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ2 ++ (m0 :: Γ5) ++ B :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m0 :: Γ5 ++ A --> B :: Γ3 ++ Γ6 = (Γ2 ++ m0 :: Γ5) ++ A --> B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ (m0 :: Γ5) ++ B :: Γ3 ++ Γ6 = (Γ2 ++ m0 :: Γ5) ++ B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ (m0 :: Γ5) ++ Γ3 ++ Γ6 = (Γ2 ++ m0 :: Γ5) ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply ImpLRule_I.
assert (Γ2 ++ Γ3 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ Γ3 ++ [] ++ (m0 :: Γ5) ++ Γ6).
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ (m0 :: Γ5) ++ Γ3 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ [] ++ Γ3 ++ Γ6).
reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert (Γ2 ++ B :: Γ3 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ (B :: Γ3) ++ [] ++ (m0 :: Γ5) ++ Γ6).
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ (m0 :: Γ5) ++ B :: Γ3 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ [] ++ (B :: Γ3) ++ Γ6).
reflexivity. rewrite H0. clear H0. apply list_exch_LI.
+ exists (Γ2 ++ m0 :: Γ4 ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ2 ++ m0 :: Γ4 ++ B :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m0 :: Γ4 ++ A --> B :: Γ3 ++ Γ6 = (Γ2 ++ m0 :: Γ4) ++ A --> B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m0 :: Γ4 ++ B :: Γ3 ++ Γ6 = (Γ2 ++ m0 :: Γ4) ++ B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m0 :: Γ4 ++ Γ3 ++ Γ6 = (Γ2 ++ m0 :: Γ4) ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert (Γ2 ++ Γ3 ++ m0 :: Γ4 ++ Γ6 = Γ2 ++ Γ3 ++ [] ++ (m0 :: Γ4) ++ Γ6).
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m0 :: Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ (m0 :: Γ4) ++ [] ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert (Γ2 ++ B :: Γ3 ++ m0 :: Γ4 ++ Γ6 = Γ2 ++ (B :: Γ3) ++ [] ++ (m0 :: Γ4) ++ Γ6).
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m0 :: Γ4 ++ B :: Γ3 ++ Γ6 = Γ2 ++ (m0 :: Γ4) ++ [] ++ (B :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
+ exists (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ B :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ A --> B :: Γ3 ++ Γ6 = (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4) ++ A --> B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ B :: Γ3 ++ Γ6 = (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4) ++ B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ Γ3 ++ Γ6 = (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4) ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply ImpLRule_I.
assert (Γ2 ++ Γ3 ++ m0 :: Γ4 ++ m1 :: Γ5 ++ Γ6 = Γ2 ++ Γ3 ++ (m0 :: Γ4) ++ (m1 :: Γ5) ++ Γ6).
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ (m1 :: Γ5) ++ (m0 :: Γ4) ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert (Γ2 ++ B :: Γ3 ++ m0 :: Γ4 ++ m1 :: Γ5 ++ Γ6 = Γ2 ++ (B :: Γ3) ++ (m0 :: Γ4) ++ (m1 :: Γ5) ++ Γ6).
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ B :: Γ3 ++ Γ6 = Γ2 ++ (m1 :: Γ5) ++ (m0 :: Γ4) ++ (B :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
- apply app2_find_hole in e0. destruct e0. repeat destruct s ; destruct p ; subst.
+ destruct Γ4 ; destruct Γ5 ; simpl ; simpl in e0 ; simpl in exch ; subst ; try inversion e0 ; 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 H0. clear H0.
assert (Γ2 ++ Γ5 ++ Γ3 ++ Γ6 = Γ2 ++ Γ5 ++ [] ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ Γ3) ++ B :: Γ5 ++ Γ6 = Γ2 ++ Γ3 ++ [] ++ (B :: Γ5) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ B :: Γ5 ++ Γ3 ++ Γ6 = Γ2 ++ (B :: Γ5) ++ [] ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. 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 H0. clear H0.
assert (Γ2 ++ Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ Γ4 ++ [] ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ Γ3) ++ B :: Γ4 ++ Γ6 = Γ2 ++ Γ3 ++ [] ++ (B :: Γ4) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ B :: Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ (B :: Γ4) ++ [] ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
* exists ((Γ2 ++ m0 :: Γ5) ++ Γ4 ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ m0 :: Γ5) ++ B :: Γ4 ++ Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m0 :: Γ5 ++ A --> B :: Γ4 ++ Γ3 ++ Γ6 = (Γ2 ++ m0 :: Γ5) ++ A --> B :: Γ4 ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert ((Γ2 ++ Γ3) ++ Γ4 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ Γ3 ++ Γ4 ++ (m0 :: Γ5) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ5) ++ Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ Γ4 ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ Γ3) ++ B :: Γ4 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ Γ3 ++ (B :: Γ4) ++ (m0 :: Γ5) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ5) ++ B :: Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ (B :: Γ4) ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
+ apply app2_find_hole in e0. destruct e0. repeat destruct s ; destruct p ; subst.
* destruct Γ5 ; simpl ; simpl in e0 ; simpl in exch ; subst ; try inversion e0 ; 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 H0. apply ImpLRule_I.
assert ((Γ2 ++ Γ3 ++ Γ4) ++ Γ1 = Γ2 ++ Γ3 ++ [] ++ Γ4 ++ Γ1). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ Γ4 ++ Γ3) ++ Γ1 = Γ2 ++ Γ4 ++ [] ++ Γ3 ++ Γ1).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ Γ3 ++ Γ4) ++ B :: Γ1 = Γ2 ++ Γ3 ++ [] ++ Γ4 ++ B :: Γ1). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ Γ4 ++ Γ3) ++ B :: Γ1 = Γ2 ++ Γ4 ++ [] ++ Γ3 ++ B :: Γ1).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. 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 H0. clear H0.
assert (Γ2 ++ B :: Γ5 ++ Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ (B :: Γ5) ++ Γ4 ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI. }
* apply app2_find_hole in e0. destruct e0. 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 H0. apply ImpLRule_I.
repeat rewrite <- app_assoc. apply list_exch_LI. repeat rewrite <- app_assoc. apply list_exch_LI. }
{ exists ((Γ2 ++ Γ5 ++ Γ4 ++ Γ3 ++ x0) ++ Γ1, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ Γ5 ++ Γ4 ++ Γ3 ++ x0) ++ B :: Γ1, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ Γ5 ++ Γ4 ++ Γ3 ++ x0 ++ A --> B :: Γ1 = (Γ2 ++ Γ5 ++ Γ4 ++ Γ3 ++ x0) ++ A --> B :: Γ1).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
repeat rewrite <- app_assoc. apply list_exch_LI. repeat rewrite <- app_assoc. apply list_exch_LI. }
{ destruct x0.
- simpl in e0. 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 H0. clear H0. apply ImpLRule_I.
repeat rewrite <- app_assoc. apply list_exch_LI. repeat rewrite <- app_assoc. apply list_exch_LI.
- inversion e0. subst.
exists ((Γ2 ++ x) ++ x0 ++ Γ4 ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ x) ++ B :: x0 ++ Γ4 ++ Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ (x ++ A --> B :: x0) ++ Γ4 ++ Γ3 ++ Γ6 = (Γ2 ++ x) ++ A --> B :: x0 ++ Γ4 ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert ((Γ2 ++ Γ3 ++ Γ4 ++ x) ++ x0 ++ Γ6 = Γ2 ++ Γ3 ++ Γ4 ++ (x ++ x0) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ x) ++ x0 ++ Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ (x ++ x0) ++ Γ4 ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply list_exch_LI.
assert ((Γ2 ++ Γ3 ++ Γ4 ++ x) ++ B :: x0 ++ Γ6 = Γ2 ++ Γ3 ++ Γ4 ++ (x ++ B :: x0) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ x) ++ B :: x0 ++ Γ4 ++ Γ3 ++ Γ6 = Γ2 ++ (x ++ B :: x0) ++ Γ4 ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply list_exch_LI. }
* destruct x ; destruct Γ5 ; simpl ; simpl in e0 ; simpl in exch ; subst ; try inversion e0 ; subst.
{ rewrite app_nil_r. exists ((Γ2 ++ x0 ++ Γ3) ++ Γ1, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ x0 ++ Γ3) ++ B :: Γ1, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ x0 ++ Γ3 ++ A --> B :: Γ1 = (Γ2 ++ x0 ++ Γ3) ++ A --> B :: Γ1).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert ((Γ2 ++ Γ3 ++ x0) ++ Γ1 = Γ2 ++ Γ3 ++ [] ++ x0 ++ Γ1).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ x0 ++ Γ3) ++ Γ1 = Γ2 ++ x0 ++ [] ++ Γ3 ++ Γ1).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ Γ3 ++ x0) ++ B :: Γ1 = Γ2 ++ Γ3 ++ [] ++ x0 ++ B :: Γ1).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ x0 ++ Γ3) ++ B :: Γ1 = Γ2 ++ x0 ++ [] ++ Γ3 ++ B :: Γ1).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI. }
{ rewrite app_nil_r. exists (Γ2 ++ Γ5 ++ x0 ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ2 ++ B :: Γ5 ++ x0 ++ Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
apply ImpLRule_I. repeat rewrite <- app_assoc. apply list_exch_LI.
assert ((Γ2 ++ Γ3 ++ x0) ++ B :: Γ5 ++ Γ6 = Γ2 ++ Γ3 ++ x0 ++ (B :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ B :: Γ5 ++ x0 ++ Γ3 ++ Γ6 = Γ2 ++ (B :: Γ5) ++ x0 ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI. }
{ exists ((Γ2 ++ x0) ++ x ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ x0) ++ B :: x ++ Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ (x0 ++ A --> B :: x) ++ Γ3 ++ Γ6 = (Γ2 ++ x0) ++ A --> B :: x ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert ((Γ2 ++ Γ3 ++ x0) ++ x ++ Γ6 = Γ2 ++ Γ3 ++ [] ++ (x0 ++ x) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ x0) ++ x ++ Γ3 ++ Γ6 = Γ2 ++ (x0 ++ x) ++ [] ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ Γ3 ++ x0) ++ B :: x ++ Γ6 = Γ2 ++ Γ3 ++ [] ++ (x0 ++ B :: x) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ x0) ++ B :: x ++ Γ3 ++ Γ6 = Γ2 ++ (x0 ++ B :: x) ++ [] ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI. }
{ exists ((Γ2 ++ m0 :: Γ5 ++ x0) ++ x ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ m0 :: Γ5 ++ x0) ++ B :: x ++ Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m0 :: Γ5 ++ (x0 ++ A --> B :: x) ++ Γ3 ++ Γ6 = (Γ2 ++ m0 :: Γ5 ++ x0) ++ A --> B :: x ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert ((Γ2 ++ Γ3 ++ x0) ++ x ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ Γ3 ++ (x0 ++ x) ++ (m0 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ5 ++ x0) ++ x ++ Γ3 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ (x0 ++ x) ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply list_exch_LI.
assert ((Γ2 ++ Γ3 ++ x0) ++ B :: x ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ Γ3 ++ (x0 ++ B :: x) ++ (m0 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ5 ++ x0) ++ B :: x ++ Γ3 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ (x0 ++ B :: x) ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply list_exch_LI. }
+ destruct x0 ; destruct Γ4 ; destruct Γ5 ; simpl ; simpl in e0 ; simpl in exch ; subst ; try inversion e0 ; 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 H0. clear H0.
assert (Γ2 ++ Γ5 ++ x ++ Γ6 = Γ2 ++ Γ5 ++ [] ++ x ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ x) ++ B :: Γ5 ++ Γ6 = Γ2 ++ x ++ [] ++ (B :: Γ5) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ B :: Γ5 ++ x ++ Γ6 = Γ2 ++ (B :: Γ5) ++ [] ++ x ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. 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 H0. clear H0.
assert (Γ2 ++ Γ4 ++ x ++ Γ6 = Γ2 ++ Γ4 ++ [] ++ x ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ x) ++ B :: Γ4 ++ Γ6 = Γ2 ++ x ++ [] ++ (B :: Γ4) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ B :: Γ4 ++ x ++ Γ6 = Γ2 ++ (B :: Γ4) ++ [] ++ x ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
* rewrite app_nil_r. exists ((Γ2 ++ m0 :: Γ5) ++ Γ4 ++ x ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ m0 :: Γ5) ++ B :: Γ4 ++ x ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m0 :: Γ5 ++ A --> B :: Γ4 ++ x ++ Γ6 = (Γ2 ++ m0 :: Γ5) ++ A --> B :: Γ4 ++ x ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert ((Γ2 ++ x) ++ Γ4 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ x ++ Γ4 ++ (m0 :: Γ5) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ5) ++ Γ4 ++ x ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ Γ4 ++ x ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ x) ++ B :: Γ4 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ x ++ (B :: Γ4) ++ (m0 :: Γ5) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ5) ++ B :: Γ4 ++ x ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ (B :: Γ4) ++ x ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_LI.
* exists ((Γ2 ++ x) ++ x0 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ x) ++ B :: x0 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ (x ++ A --> B :: x0) ++ Γ6 = (Γ2 ++ x) ++ A --> B :: x0 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
apply list_exch_L_id. apply list_exch_L_id.
* exists ((Γ2 ++ m0 :: Γ5 ++ x) ++ x0 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ m0 :: Γ5 ++ x) ++ B :: x0 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m0 :: Γ5 ++ (x ++ A --> B :: x0) ++ Γ6 = (Γ2 ++ m0 :: Γ5 ++ x) ++ A --> B :: x0 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert ((Γ2 ++ x) ++ x0 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ [] ++ (x ++ x0) ++ (m0 :: Γ5) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ5 ++ x) ++ x0 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ (x ++ x0) ++ [] ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ x) ++ B :: x0 ++ m0 :: Γ5 ++ Γ6 = Γ2 ++ [] ++ (x ++ B :: x0) ++ (m0 :: Γ5) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ5 ++ x) ++ B :: x0 ++ Γ6 = Γ2 ++ (m0 :: Γ5) ++ (x ++ B :: x0) ++ [] ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
* exists ((Γ2 ++ m0 :: Γ4 ++ x) ++ x0 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ m0 :: Γ4 ++ x) ++ B :: x0 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m0 :: Γ4 ++ (x ++ A --> B :: x0) ++ Γ6 = (Γ2 ++ m0 :: Γ4 ++ x) ++ A --> B :: x0 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert ((Γ2 ++ x) ++ x0 ++ m0 :: Γ4 ++ Γ6 = Γ2 ++ [] ++ (x ++ x0) ++ (m0 :: Γ4) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ4 ++ x) ++ x0 ++ Γ6 = Γ2 ++ (m0 :: Γ4) ++ (x ++ x0) ++ [] ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ x) ++ B :: x0 ++ m0 :: Γ4 ++ Γ6 = Γ2 ++ [] ++ (x ++ B :: x0) ++ (m0 :: Γ4) ++ Γ6). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m0 :: Γ4 ++ x) ++ B :: x0 ++ Γ6 = Γ2 ++ (m0 :: Γ4) ++ (x ++ B :: x0) ++ [] ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
* exists ((Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ x) ++ x0 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ x) ++ B :: x0 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ (x ++ A --> B :: x0) ++ Γ6 = (Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ x) ++ A --> B :: x0 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. simpl.
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert ((Γ2 ++ x) ++ x0 ++ m0 :: Γ4 ++ m1 :: Γ5 ++ Γ6 = Γ2 ++ (x ++ x0) ++ (m0 :: Γ4) ++ (m1 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ x) ++ x0 ++ Γ6 = Γ2 ++ (m1 :: Γ5) ++ (m0 :: Γ4) ++ (x ++ x0) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ2 ++ x) ++ B :: x0 ++ m0 :: Γ4 ++ m1 :: Γ5 ++ Γ6 = Γ2 ++ (x ++ B :: x0) ++ (m0 :: Γ4) ++ (m1 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ2 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ x) ++ B :: x0 ++ Γ6 = Γ2 ++ (m1 :: Γ5) ++ (m0 :: Γ4) ++ (x ++ B :: x0) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
- destruct x ; destruct Γ3 ; destruct Γ4 ; destruct Γ5 ; simpl ; simpl in e0 ; simpl in exch ;
subst ; try inversion e0 ; 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 ++ m0 :: Γ5) ++ Γ4 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ0 ++ m0 :: Γ5) ++ B :: Γ4 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ0 ++ m0 :: Γ5 ++ A --> B :: Γ4 ++ Γ6 = (Γ0 ++ m0 :: Γ5) ++ A --> B :: Γ4 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert (Γ0 ++ Γ4 ++ m0 :: Γ5 ++ Γ6 = Γ0 ++ [] ++ Γ4 ++ (m0 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ0 ++ m0 :: Γ5) ++ Γ4 ++ Γ6 = Γ0 ++ (m0 :: Γ5) ++ Γ4 ++ [] ++ Γ6).
repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert (Γ0 ++ B :: Γ4 ++ m0 :: Γ5 ++ Γ6 = Γ0 ++ [] ++ (B :: Γ4) ++ (m0 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ0 ++ m0 :: Γ5) ++ B :: Γ4 ++ Γ6 = Γ0 ++ (m0 :: Γ5) ++ (B :: Γ4) ++ [] ++ Γ6).
repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. 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 ++ m0 :: Γ5) ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ0 ++ m0 :: Γ5) ++ B :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ0 ++ m0 :: Γ5 ++ A --> B :: Γ3 ++ Γ6 = (Γ0 ++ m0 :: Γ5) ++ A --> B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert (Γ0 ++ Γ3 ++ m0 :: Γ5 ++ Γ6 = Γ0 ++ [] ++ Γ3 ++ (m0 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ0 ++ m0 :: Γ5) ++ Γ3 ++ Γ6 = Γ0 ++ (m0 :: Γ5) ++ Γ3 ++ [] ++ Γ6).
repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert (Γ0 ++ B :: Γ3 ++ m0 :: Γ5 ++ Γ6 = Γ0 ++ [] ++ (B :: Γ3) ++ (m0 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ0 ++ m0 :: Γ5) ++ B :: Γ3 ++ Γ6 = Γ0 ++ (m0 :: Γ5) ++ (B :: Γ3) ++ [] ++ Γ6).
repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
* rewrite app_nil_r. exists ((Γ0 ++ m0 :: Γ4) ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ0 ++ m0 :: Γ4) ++ B :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ0 ++ m0 :: Γ4 ++ A --> B :: Γ3 ++ Γ6 = (Γ0 ++ m0 :: Γ4) ++ A --> B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert ((Γ0 ++ m0 :: Γ4) ++ Γ3 ++ Γ6 = Γ0 ++ (m0 :: Γ4) ++ Γ3 ++ [] ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ Γ3 ++ m0 :: Γ4 ++ Γ6 = Γ0 ++ [] ++ Γ3 ++ (m0 :: Γ4) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert ((Γ0 ++ m0 :: Γ4) ++ B :: Γ3 ++ Γ6 = Γ0 ++ (m0 :: Γ4) ++ (B :: Γ3) ++ [] ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ B :: Γ3 ++ m0 :: Γ4 ++ Γ6 = Γ0 ++ [] ++ (B :: Γ3) ++ (m0 :: Γ4) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
* rewrite app_nil_r. exists ((Γ0 ++ m1 :: Γ5 ++ m0 :: Γ4) ++ Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists ((Γ0 ++ m1 :: Γ5 ++ m0 :: Γ4) ++ B :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
assert (Γ0 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ A --> B :: Γ3 ++ Γ6 = (Γ0 ++ m1 :: Γ5 ++ m0 :: Γ4) ++ A --> B :: Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply ImpLRule_I.
assert (Γ0 ++ Γ3 ++ m0 :: Γ4 ++ m1 :: Γ5 ++ Γ6 = Γ0 ++ Γ3 ++ (m0 :: Γ4) ++ (m1 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ0 ++ m1 :: Γ5 ++ m0 :: Γ4) ++ Γ3 ++ Γ6 = Γ0 ++ (m1 :: Γ5) ++ (m0 :: Γ4) ++ Γ3 ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert (Γ0 ++ B :: Γ3 ++ m0 :: Γ4 ++ m1 :: Γ5 ++ Γ6 = Γ0 ++ (B :: Γ3) ++ (m0 :: Γ4) ++ (m1 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert ((Γ0 ++ m1 :: Γ5 ++ m0 :: Γ4) ++ B :: Γ3 ++ Γ6 = Γ0 ++ (m1 :: Γ5) ++ (m0 :: Γ4) ++ (B :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. 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 ++ m0 :: Γ5 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ0 ++ B :: x ++ m0 :: Γ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 ++ m0 :: Γ4 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ0 ++ B :: x ++ m0 :: Γ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 ++ m1 :: Γ5 ++ m0 :: Γ4 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ0 ++ B :: x ++ m1 :: Γ5 ++ m0 :: Γ4 ++ Γ6, Δ0 ++ Δ1). split. split.
repeat rewrite <- app_assoc. apply ImpLRule_I.
assert (Γ0 ++ x ++ m0 :: Γ4 ++ m1 :: Γ5 ++ Γ6 = (Γ0 ++ x) ++ (m0 :: Γ4) ++ [] ++ (m1 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ x ++ m1 :: Γ5 ++ m0 :: Γ4 ++ Γ6 = (Γ0 ++ x) ++ (m1 :: Γ5) ++ [] ++ (m0 :: Γ4) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert (Γ0 ++ B :: x ++ m0 :: Γ4 ++ m1 :: Γ5 ++ Γ6 = (Γ0 ++ B :: x) ++ (m0 :: Γ4) ++ [] ++ (m1 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ B :: x ++ m1 :: Γ5 ++ m0 :: Γ4 ++ Γ6 = (Γ0 ++ B :: x) ++ (m1 :: Γ5) ++ [] ++ (m0 :: Γ4) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
* exists (Γ0 ++ x ++ m0 :: Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ0 ++ B :: x ++ m0 :: Γ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 ++ m1 :: Γ5 ++ m0 :: Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ0 ++ B :: x ++ m1 :: Γ5 ++ m0 :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
repeat rewrite <- app_assoc. apply ImpLRule_I.
assert (Γ0 ++ x ++ m0 :: Γ3 ++ m1 :: Γ5 ++ Γ6 = (Γ0 ++ x) ++ (m0 :: Γ3) ++ [] ++ (m1 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ x ++ m1 :: Γ5 ++ m0 :: Γ3 ++ Γ6 = (Γ0 ++ x) ++ (m1 :: Γ5) ++ [] ++ (m0 :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert (Γ0 ++ B :: x ++ m0 :: Γ3 ++ m1 :: Γ5 ++ Γ6 = (Γ0 ++ B :: x) ++ (m0 :: Γ3) ++ [] ++ (m1 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ B :: x ++ m1 :: Γ5 ++ m0 :: Γ3 ++ Γ6 = (Γ0 ++ B :: x) ++ (m1 :: Γ5) ++ [] ++ (m0 :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
* exists (Γ0 ++ x ++ m1 :: Γ4 ++ m0 :: Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ0 ++ B :: x ++ m1 :: Γ4 ++ m0 :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
repeat rewrite <- app_assoc. apply ImpLRule_I.
assert (Γ0 ++ x ++ m0 :: Γ3 ++ m1 :: Γ4 ++ Γ6 = (Γ0 ++ x) ++ (m0 :: Γ3) ++ [] ++ (m1 :: Γ4) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ x ++ m1 :: Γ4 ++ m0 :: Γ3 ++ Γ6 = (Γ0 ++ x) ++ (m1 :: Γ4) ++ [] ++ (m0 :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert (Γ0 ++ B :: x ++ m0 :: Γ3 ++ m1 :: Γ4 ++ Γ6 = (Γ0 ++ B :: x) ++ (m0 :: Γ3) ++ [] ++ (m1 :: Γ4) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ B :: x ++ m1 :: Γ4 ++ m0 :: Γ3 ++ Γ6 = (Γ0 ++ B :: x) ++ (m1 :: Γ4) ++ [] ++ (m0 :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
* exists (Γ0 ++ x ++ m2 :: Γ5 ++ m1 :: Γ4 ++ m0 :: Γ3 ++ Γ6, Δ0 ++ A :: Δ1).
exists (Γ0 ++ B :: x ++ m2 :: Γ5 ++ m1 :: Γ4 ++ m0 :: Γ3 ++ Γ6, Δ0 ++ Δ1). split. split.
repeat rewrite <- app_assoc. apply ImpLRule_I.
assert (Γ0 ++ x ++ m0 :: Γ3 ++ m1 :: Γ4 ++ m2 :: Γ5 ++ Γ6 = (Γ0 ++ x) ++ (m0 :: Γ3) ++ (m1 :: Γ4) ++ (m2 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ x ++ m2 :: Γ5 ++ m1 :: Γ4 ++ m0 :: Γ3 ++ Γ6 = (Γ0 ++ x) ++ (m2 :: Γ5) ++ (m1 :: Γ4) ++ (m0 :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
assert (Γ0 ++ B :: x ++ m0 :: Γ3 ++ m1 :: Γ4 ++ m2 :: Γ5 ++ Γ6 = (Γ0 ++ B :: x) ++ (m0 :: Γ3) ++ (m1 :: Γ4) ++ (m2 :: Γ5) ++ Γ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ B :: x ++ m2 :: Γ5 ++ m1 :: Γ4 ++ m0 :: Γ3 ++ Γ6 = (Γ0 ++ B :: x) ++ (m2 :: Γ5) ++ (m1 :: Γ4) ++ (m0 :: Γ3) ++ Γ6).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply list_exch_LI.
Qed.
Lemma ImpL_app_list_exchR : forall s se ps1 ps2,
(@list_exch_R s se) ->
(ImpLRule [ps1;ps2] s) ->
(existsT2 pse1 pse2,
(ImpLRule [pse1;pse2] se) *
(@list_exch_R ps1 pse1) *
(@list_exch_R ps2 pse2)).
Proof.
intros s se ps1 ps2 exch. intro RA. inversion RA. inversion exch. subst.
inversion H. apply app2_find_hole in H2. destruct H2. 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 H0. clear H0.
assert (Δ2 ++ A :: Δ5 ++ Δ4 ++ Δ3 ++ Δ6 = (Δ2 ++ [A]) ++ Δ5 ++ Δ4 ++ Δ3 ++ Δ6).
rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_RI.
apply list_exch_RI.
- apply app2_find_hole in e0. destruct e0. 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 H0. clear H0. apply ImpLRule_I.
repeat rewrite <- app_assoc.
assert (Δ2 ++ Δ3 ++ A :: Δ4 ++ Δ5 ++ Δ6 = Δ2 ++ Δ3 ++ (A :: Δ4) ++ Δ5 ++ Δ6).
reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ Δ5 ++ A :: Δ4 ++ Δ3 ++ Δ6 = Δ2 ++ Δ5 ++ (A :: Δ4) ++ Δ3 ++ Δ6).
reflexivity. rewrite H0. clear H0. apply list_exch_RI. apply list_exch_RI.
+ apply app2_find_hole in e0. destruct e0. 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 H0. clear H0. 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 H0. clear H0.
assert (Δ2 ++ Δ5 ++ Δ4 ++ A :: Δ3 ++ Δ6 = Δ2 ++ Δ5 ++ (Δ4 ++ [A]) ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_RI. apply list_exch_RI.
* apply app2_find_hole in e0. destruct e0. 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 ++ x0 ++ A :: Δ1).
exists (Γ0 ++ B :: Γ1, Δ2 ++ Δ5 ++ Δ4 ++ Δ3 ++ x0 ++ Δ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 :: x0) ++ Δ4 ++ Δ3 ++ Δ6).
exists (Γ0 ++ B :: Γ1, Δ2 ++ x ++ x0 ++ Δ4 ++ Δ3 ++ Δ6). split. split.
assert (Δ2 ++ (x ++ A :: x0) ++ Δ4 ++ Δ3 ++ Δ6 = (Δ2 ++ x) ++ A :: x0 ++ Δ4 ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ x ++ x0 ++ Δ4 ++ Δ3 ++ Δ6 = (Δ2 ++ x) ++ x0 ++ Δ4 ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply ImpLRule_I.
assert (Δ2 ++ Δ3 ++ Δ4 ++ x ++ A :: x0 ++ Δ6 = Δ2 ++ Δ3 ++ Δ4 ++ (x ++ A :: x0) ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply list_exch_RI.
assert (Δ2 ++ Δ3 ++ Δ4 ++ x ++ x0 ++ Δ6 = Δ2 ++ Δ3 ++ Δ4 ++ (x ++ x0) ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ x ++ x0 ++ Δ4 ++ Δ3 ++ Δ6 = Δ2 ++ (x ++ x0) ++ Δ4 ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply list_exch_RI. }
* repeat rewrite <- app_assoc. exists (Γ0 ++ Γ1, Δ2 ++ Δ5 ++ (x0 ++ A :: x) ++ Δ3 ++ Δ6).
exists (Γ0 ++ B :: Γ1, Δ2 ++ Δ5 ++ (x0 ++ x) ++ Δ3 ++ Δ6). split. split.
assert (Δ2 ++ Δ5 ++ (x0 ++ A :: x) ++ Δ3 ++ Δ6 = (Δ2 ++ Δ5 ++ x0) ++ A :: x ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ Δ5 ++ x0 ++ x ++ Δ3 ++ Δ6 = (Δ2 ++ Δ5 ++ x0) ++ x ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ Δ5 ++ (x0 ++ x) ++ Δ3 ++ Δ6 = (Δ2 ++ Δ5 ++ x0) ++ x ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply ImpLRule_I.
assert (Δ2 ++ Δ3 ++ x0 ++ A :: x ++ Δ5 ++ Δ6 = Δ2 ++ Δ3 ++ (x0 ++ A :: x) ++ Δ5 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply list_exch_RI.
assert (Δ2 ++ Δ3 ++ x0 ++ x ++ Δ5 ++ Δ6 = Δ2 ++ Δ3 ++ (x0 ++ x) ++ Δ5 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply list_exch_RI.
+ repeat rewrite <- app_assoc. exists (Γ0 ++ Γ1, Δ2 ++ Δ5 ++ Δ4 ++ (x ++ A :: x0) ++ Δ6).
exists (Γ0 ++ B :: Γ1, Δ2 ++ Δ5 ++ Δ4 ++ (x ++ x0) ++ Δ6). split. split.
assert (Δ2 ++ Δ5 ++ Δ4 ++ (x ++ A :: x0) ++ Δ6 = (Δ2 ++ Δ5 ++ Δ4 ++ x) ++ A :: x0 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ Δ5 ++ Δ4 ++ x ++ x0 ++ Δ6 = (Δ2 ++ Δ5 ++ Δ4 ++ x) ++ x0 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ Δ5 ++ Δ4 ++ (x ++ x0) ++ Δ6 = (Δ2 ++ Δ5 ++ Δ4 ++ x) ++ x0 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply ImpLRule_I.
assert (Δ2 ++ x ++ A :: x0 ++ Δ4 ++ Δ5 ++ Δ6 = Δ2 ++ (x ++ A :: x0) ++ Δ4 ++ Δ5 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. apply list_exch_RI.
assert (Δ2 ++ x ++ x0 ++ Δ4 ++ Δ5 ++ Δ6 = Δ2 ++ (x ++ x0) ++ Δ4 ++ Δ5 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. 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 H0. clear H0.
assert (Δ0 ++ A :: x ++ Δ5 ++ Δ4 ++ Δ3 ++ Δ6 = (Δ0 ++ A :: x) ++ Δ5 ++ Δ4 ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_RI.
assert (Δ0 ++ x ++ Δ3 ++ Δ4 ++ Δ5 ++ Δ6 = (Δ0 ++ x) ++ Δ3 ++ Δ4 ++ Δ5 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Δ0 ++ x ++ Δ5 ++ Δ4 ++ Δ3 ++ Δ6 = (Δ0 ++ x) ++ Δ5 ++ Δ4 ++ Δ3 ++ Δ6).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply list_exch_RI.
Qed.