(****************************************************************************)
(*                                                                          *)
(*                The formal system \lambda\delta                           *)
(*                                                                          *)
(*                Author: Ferruccio Guidi                                   *)
(*                                                                          *)
(*                This file is distributed under the terms of the           *)
(*                GNU General Public License Version 2                      *)
(*                                                                          *)
(****************************************************************************)

Require Export contexts_defs.
Require Export subst0_defs.
Require Export getl_defs.

      Inductive csubst0: nat -> T -> C -> C -> Prop :=
         | csubst0_snd:  (k:?; i:?; v,u1,u2:?) (subst0 i v u1 u2) -> (c:?)
                         (csubst0 (s k i) v (CHead c k u1) (CHead c k u2))
         | csubst0_fst:  (k:?; i:?; c1,c2:?; v:?) (csubst0 i v c1 c2) ->
                         (u:?) (csubst0 (s k i) v (CHead c1 k u) (CHead c2 k u))
         | csubst0_both: (k:?; i:?; v,u1,u2:?) (subst0 i v u1 u2) ->
                         (c1,c2:?) (csubst0 i v c1 c2) ->
                         (csubst0 (s k i) v (CHead c1 k u1) (CHead c2 k u2)).

      Hint csubst0 : ld := Constructors csubst0.

   Section csubst0_props. (**************************************************)

      Lemma csubst0_snd_bind: (b:?; i:?; v,u1,u2:?) (subst0 i v u1 u2) ->
                              (c:?) (csubst0 (S i) v (CHead c (Bind b) u1) (CHead c (Bind b) u2)).
      Proof.
      Intros; Replace (S i) with (s (Bind b) i); XAuto.
      Qed.

      Lemma csubst0_fst_bind: (b:?; i:?; c1,c2:?; v:?) (csubst0 i v c1 c2) ->
                              (u:?) (csubst0 (S i) v (CHead c1 (Bind b) u) (CHead c2 (Bind b) u)).
      Proof.
      Intros; Replace (S i) with (s (Bind b) i); XAuto.
      Qed.

      Theorem csubst0_both_bind: (b:?; i:?; v,u1,u2:?) (subst0 i v u1 u2) ->
                                 (c1,c2:?) (csubst0 i v c1 c2) ->
                                 (csubst0 (S i) v (CHead c1 (Bind b) u1) (CHead c2 (Bind b) u2)).
      Proof.
      Intros; Replace (S i) with (s (Bind b) i); XAuto.
      Qed.

   End csubst0_props.

      Hints Resolve csubst0_snd_bind csubst0_fst_bind csubst0_both_bind : ld.

   Section csubst0_gen_base. (***********************************************)

      Lemma csubst0_gen_sort: (x:?; v:?; i,n:?) (csubst0 i v (CSort n) x) ->
                              (P:Prop) P.
      Proof.
      Intros; InsertEq H '(CSort n); XElim H; Clear i v y x;
      Intros; XInv.
      Qed.

      Lemma csubst0_gen_head: (k:?; c1,x:?; u1,v:?; i:?)
                              (csubst0 i v (CHead c1 k u1) x) -> (OR
                              (EX u2 j | i = (s k j) &
                                         x = (CHead c1 k u2) &
                                         (subst0 j v u1 u2)
                              ) |
                              (EX c2 j | i = (s k j) &
                                         x = (CHead c2 k u1) &
                                         (csubst0 j v c1 c2)
                              ) |
                              (EX u2 c2 j | i = (s k j) &
                                            x = (CHead c2 k u2) &
                                            (subst0 j v u1 u2) &
                                            (csubst0 j v c1 c2)
                              )).
      Proof.
      Intros; InsertEq H '(CHead c1 k u1); XElim H; Clear i v y x;
      Intros; XInv; Subst; XDEAuto 3.
      Qed.

   End csubst0_gen_base.

      Tactic Definition CSubst0GenBase := (
         Match Context With
            | [ H: (csubst0 ?1 ?2 (CSort ?3) ?4) |- ? ] ->
               EApply csubst0_gen_sort; Apply H
            | [ H: (csubst0 ?1 ?2 (CHead ?3 ?4 ?5) ?6) |- ? ] ->
               LApply (csubst0_gen_head ?4 ?3 ?6 ?5 ?2 ?1); [ Clear H; Intros H | XAuto ];
               XDecompose H
         ).

   Section csubst0_gen. (****************************************************)

      Lemma csubst0_gen_S_bind_2: (b:?; x,c2:?; v,v2:?; i:?)
                                  (csubst0 (S i) v x (CHead c2 (Bind b) v2)) -> (OR
                                  (EX v1 | (subst0 i v v1 v2) & x = (CHead c2 (Bind b) v1)) |
                                  (EX c1 | (csubst0 i v c1 c2) & x = (CHead c1 (Bind b) v2)) |
                                  (EX c1 v1 | (subst0 i v v1 v2) & (csubst0 i v c1 c2) &
                                              x = (CHead c1 (Bind b) v1)
                                  )).
      Proof.
      XElim x; Intros; CSubst0GenBase; Clear H; Do 2 (XInv; Subst); XDEAuto 3.
      Qed.

   End csubst0_gen.

      Tactic Definition CSubst0Gen := (
         Match Context With
            | [ H: (csubst0 (S ?) ? ? (CHead ? (Bind ?) ?)) |- ? ] ->
               XDecomPoseClear H '(csubst0_gen_S_bind_2 ? ? ? ? ? ? H)
            | [ |- ? ] -> CSubst0GenBase
         ).

   Section csubst0_drop. (***************************************************)

      Lemma csubst0_drop_gt: (n,i:?) (lt i n) ->
                             (c1,c2:?; v:?) (csubst0 i v c1 c2) ->
                             (e:?) (drop n (0) c1 e) -> (drop n (0) c2 e).
      Proof.
      XElim n.
(* case 1: n = 0 *)
      Intros; LeLtGen.
(* case 2: n > 0 *)
      XElim c1; Intros; DropGenBase; Subst; Do 2 XInv.
(* case 2.2: CHead k *)
      CSubst0GenBase; Subst; NewInduction k;
      Simpl in H0; Try LeLtGen; XDEAuto 3.
      Qed.

      Lemma csubst0_drop_gt_back: (n,i:?) (lt i n) ->
                                  (c1,c2:?; v:?) (csubst0 i v c1 c2) ->
                                  (e:?) (drop n (0) c2 e) ->
                                  (drop n (0) c1 e).
      Proof.
      XElim n.
(* case 1: n = 0 *)
      Intros; LeLtGen.
(* case 2: n > 0 *)
      XElim c1; Intros; CSubst0GenBase; Subst;
(* case 2.2: CHead k *)
      DropGenBase; NewInduction k; Simpl in H0; LeLtGen; XDEAuto 3.
      Qed.

      Hint discr : ld := Extern 4 (subst0 ? ? ? ?) SRw; Simpl.

      Hint discr : ld := Extern 4 (csubst0 ? ? ? ?) SRw; Simpl.

      Hints Resolve le_S_n : ld.

      Lemma csubst0_drop_lt: (n,i:?) (lt n i) ->
                             (c1,c2:?; v:?) (csubst0 i v c1 c2) ->
                             (e:?) (drop n (0) c1 e) -> (OR
                             (drop n (0) c2 e) |
                             (EX k e0 u w | e = (CHead e0 k u) &
                                            (drop n (0) c2 (CHead e0 k w)) &
                                            (subst0 (minus i (s k n)) v u w)
                             ) |
                             (EX k e1 e2 u | e = (CHead e1 k u) &
                                             (drop n (0) c2 (CHead e2 k u)) &
                                             (csubst0 (minus i (s k n)) v e1 e2)
                             ) |
                             (EX k e1 e2 u w | e = (CHead e1 k u) &
                                               (drop n (0) c2 (CHead e2 k w)) &
                                               (subst0 (minus i (s k n)) v u w) &
                                                 (csubst0 (minus i (s k n)) v e1 e2)
                             )).
      Proof.
      XElim n.
(* case 1: n = 0 *)
      Intros; DropGenBase; Subst.
      XElim H0; Clear v c1 c2; Intros;
      Rewrite <- (s_arith0 k i0) in H0;
      Try Rewrite <- (s_arith0 k i0) in H1; XDEAuto 3.
(* case 2: n > 0 *)
      Intros n IHn; XElim c1; Intros;
      DropGenBase; Subst.
(* case 2.1: CSort *)
      Do 2 XInv.
(* case 2.2: CHead k *)
      CSubst0GenBase; Subst;
      (NewInduction k; [ Clear H0 | Clear IHn H ]).
(* case 2.2.1: csubst0_snd, Bind *)
      XDEAuto 3.
(* case 2.2.2: csubst0_snd, Flat *)
      XDEAuto 3.
(* case 2.2.3: csubst0_fst, Bind *)
      LApply (IHn x1); [ Clear IHn H; Intros IHn | XAuto ].
      LApply (IHn c x0 v); [ Clear IHn H4; Intros IHn | XAuto ].
      LApply (IHn e); [ Clear IHn H2; Intros IHn | XAuto ].
      XDecompose IHn; Subst; XDEAuto 6.
(* case 2.2.4: csubst0_fst, Flat *)
      LApply (H0 x0 v); [ Clear H0 H4; Intros H0 | XAuto ].
      LApply (H0 e); [ Clear H0 H2; Intros H0 | XAuto ].
      XDecompose H0; Subst; XDEAuto 4.
(* case 2.2.5: csubst0_both, Bind *)
      LApply (IHn x2); [ Clear IHn H; Intros IHn | XAuto ].
      LApply (IHn c x1 v); [ Clear IHn H5; Intros IHn | XAuto ].
      LApply (IHn e); [ Clear IHn H2; Intros IHn | XAuto ].
      XDecompose IHn; Subst; XDEAuto 6.
(* case 2.2.6: csubst0_both Flat *)
      LApply (H0 x1 v); [ Clear H0 H5; Intros H0 | XAuto ].
      LApply (H0 e); [ Clear H0 H2; Intros H0 | XAuto ].
      XDecompose H0; Subst; XDEAuto 4.
      Qed.

      Lemma csubst0_drop_eq: (n:?; c1,c2:?; v:?) (csubst0 n v c1 c2) ->
                             (e:?) (drop n (0) c1 e) -> (OR
                             (drop n (0) c2 e) |
                             (EX f e0 u w | e = (CHead e0 (Flat f) u) &
                                            (drop n (0) c2 (CHead e0 (Flat f) w)) &
                                            (subst0 (0) v u w)
                             ) |
                             (EX f e1 e2 u | e = (CHead e1 (Flat f) u) &
                                             (drop n (0) c2 (CHead e2 (Flat f) u)) &
                                             (csubst0 (0) v e1 e2)
                             ) |
                             (EX f e1 e2 u w | e = (CHead e1 (Flat f) u) &
                                               (drop n (0) c2 (CHead e2 (Flat f) w)) &
                                               (subst0 (0) v u w) &
                                               (csubst0 (0) v e1 e2)
                             )).
      Proof.
      XElim n.
(* case 1: n = 0 *)
      Intros; DropGenBase; Subst.
      InsertEq H '(0); XElim H; Clear y v c1 c2;
      (XElim k; Simpl; Intros; [ XInv | Subst; XDEAuto 3 ]).
(* case 2: n > 0 *)
      Intros n IHn; XElim c1; Intros;
      DropGenBase; Subst.
(* case 2.1: CSort *)
      Do 2 XInv.
(* case 2.2: CHead k *)
      CSubst0GenBase; Subst;
      (NewInduction k; Simpl in H1; XInv; Subst; [ Clear H | Clear IHn ]).
(* case 2.2.1: csubst0_snd, Bind *)
      XDEAuto 4.
(* case 2.2.2: csubst0_snd, Flat *)
      XDEAuto 4.
(* case 2.2.3: csubst0_fst, Bind *)
      LApply (IHn c x0 v); [ Clear IHn H3; Intros IHn | XAuto ].
      LApply (IHn e); [ Clear IHn H1; Intros IHn | XAuto ].
      XDecompose IHn; Subst; XDEAuto 6.
(* case 2.2.4: csubst0_fst, Flat *)
      LApply (H x0 v); [ Clear H H3; Intros H | XAuto ].
      LApply (H e); [ Clear H H1; Intros H | XAuto ].
      XDecompose H; Subst; XDEAuto 5.
(* case 2.2.5: csubst0_both, Bind *)
      LApply (IHn c x1 v); [ Clear IHn H3 H4; Intros IHn | XAuto ].
      LApply (IHn e); [ Clear IHn H1; Intros IHn | XAuto ].
      XDecompose IHn; Subst; XDEAuto 6.
(* case 2.2.6: csubst0_both Flat *)
      LApply (H x1 v); [ Clear H H3 H4; Intros H | XAuto ].
      LApply (H e); [ Clear H H1; Intros H | XAuto ].
      XDecompose H; Subst; XDEAuto 5.
      Qed.

      Lemma csubst0_drop_eq_back: (n:?; c1,c2:?; v:?) (csubst0 n v c1 c2) ->
                                  (e:?) (drop n (0) c2 e) -> (OR
                                  (drop n (0) c1 e) |
                                  (EX f e0 u1 u2 | e = (CHead e0 (Flat f) u2) &
                                                 (drop n (0) c1 (CHead e0 (Flat f) u1)) &
                                                 (subst0 (0) v u1 u2)
                                  ) |
                                  (EX f e1 e2 u | e = (CHead e2 (Flat f) u) &
                                                  (drop n (0) c1 (CHead e1 (Flat f) u)) &
                                                  (csubst0 (0) v e1 e2)
                                  ) |
                                  (EX f e1 e2 u1 u2 | e = (CHead e2 (Flat f) u2) &
                                                      (drop n (0) c1 (CHead e1 (Flat f) u1)) &
                                                      (subst0 (0) v u1 u2) &
                                                      (csubst0 (0) v e1 e2)
                                  )).
      Proof.
      XElim n.
(* case 1: n = 0 *)
      Intros; DropGenBase; Subst.
      InsertEq H '(0); XElim H; Clear y v c1 c2;
      (XElim k; Simpl; Intros; [ XInv | Subst; XDEAuto 3 ]).
(* case 2: n > 0 *)
      Intros n IHn; XElim c1; Intros;
      CSubst0GenBase; Subst; DropGenBase;
      (NewInduction k; Simpl in H0; XInv; Subst; [ Clear H | Clear IHn ]).
(* case 2.2.1: csubst0_snd, Bind *)
      XDEAuto 3.
(* case 2.2.2: csubst0_snd, Flat *)
      XDEAuto 3.
(* case 2.2.3: csubst0_fst, Bind *)
      LApply (IHn c x0 v); [ Clear IHn H3; Intros IHn | XAuto ].
      LApply (IHn e); [ Clear IHn H1; Intros IHn | XAuto ].
      XDecompose IHn; Subst; XDEAuto 6.
(* case 2.2.4: csubst0_fst, Flat *)
      LApply (H x0 v); [ Clear H H3; Intros H | XAuto ].
      LApply (H e); [ Clear H H1; Intros H | XAuto ].
      XDecompose H; Subst; XDEAuto 4.
(* case 2.2.5: csubst0_both, Bind *)
      LApply (IHn c x1 v); [ Clear IHn H3 H4; Intros IHn | XAuto ].
      LApply (IHn e); [ Clear IHn H1; Intros IHn | XAuto ].
      XDecompose IHn; Subst; XDEAuto 6.
(* case 2.2.6: csubst0_both Flat *)
      LApply (H x1 v); [ Clear H H3 H4; Intros H | XAuto ].
      LApply (H e); [ Clear H H1; Intros H | XAuto ].
      XDecompose H; Subst; XDEAuto 4.
      Qed.

      Lemma csubst0_drop_lt_back: (n,i:?) (lt n i) ->
                                  (c1,c2:?; v:?) (csubst0 i v c1 c2) ->
                                  (e2:?) (drop n O c2 e2) ->
                                  (drop n O c1 e2) \/
                                  (EX e1 | (csubst0 (minus i n) v e1 e2) &
                                           (drop n O c1 e1)
                                  ).
      Proof.
      XElim n.
(* case 1: n = 0 *)
      Intros; DropGenBase; Subst.
      Rewrite <- minus_n_O; XDEAuto 3.
(* case 2: n > 0 *)
      Intros n IHn; XElim c1; Intros;
      CSubst0GenBase; Subst; DropGenBase;
      (NewInduction k; [ Simpl in H; LeLtGen; Clear H0 | Clear IHn H ]).
(* case 2.2.1: csubst0_snd, Bind *)
      XDEAuto 3.
(* case 2.2.2: csubst0_snd, Flat *)
      XDEAuto 3.
(* case 2.2.3: csubst0_fst, Bind *)
      XDecomPoseClear IHn '(IHn ? H ? ? ? H6 ? H1); Clear H H6 H1; XDEAuto 4.
(* case 2.2.4: csubst0_fst, Flat *)
      XDecomPoseClear H0 '(H0 ? ? H6 ? H1); Clear H6 H1; XDEAuto 4.
(* case 2.2.5: csubst0_both, Bind *)
      XDecomPoseClear IHn '(IHn ? H ? ? ? H7 ? H1); Clear H H7 H1; XDEAuto 4.
(* case 2.2.6: csubst0_both Flat *)
      XDecomPoseClear H0 '(H0 ? ? H7 ? H1); Clear H7 H1; XDEAuto 4.
      Qed.

   End csubst0_drop.

      Tactic Definition CSubst0Drop := (
         Match Context With
            | [ H1: (lt ?1 ?2);
                H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?2 (0) ?4 ?6) |- ? ] ->
               LApply (csubst0_drop_gt ?2 ?1); [ Intros H_x | XAuto ];
               LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
               LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ]
            | [ H1: (lt ?2 ?1);
                H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?2 (0) ?4 ?6) |- ? ] ->
               LApply (csubst0_drop_lt ?2 ?1); [ Intros H_x | XAuto ];
               LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
               LApply (H_x ?6); [ Clear H_x H3; Intros H_x | XAuto ];
               XDecompose H_x
            | [ H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?1 (0) ?4 ?6) |- ? ] ->
               LApply (csubst0_drop_eq ?1 ?4 ?5 ?3); [ Clear H_x H2; Intros H2 | XAuto ];
               LApply (H2 ?6); [ Clear H2 H3; Intros H_x | XAuto ];
               XDecompose H_x
            | [ H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?2 (0) ?5 ?6) |- ? ] ->
               LApply (csubst0_drop_gt_back ?2 ?1); [ Intros H_x | XAuto ];
               LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
               LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ]
            | [ H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?1 (0) ?5 ?6) |- ? ] ->
               LApply (csubst0_drop_eq_back ?1 ?4 ?5 ?3); [ Clear H_x H2; Intros H2 | XAuto ];
               LApply (H2 ?6); [ Clear H2 H3; Intros H_x | XAuto ];
               XDecompose H_x
            | [ H1: (lt ?2 ?1);
                H2: (csubst0 ?1 ? ? ?0); H3: (drop ?2 (0) ?0 ?) |- ? ] ->
               XDecomPoseClear H3 '(csubst0_drop_lt_back ? ? H1 ? ? ? H2 ? H3)
         ).

   Section csubst0_clear. (**************************************************)

      Lemma csubst0_clear_O: (c1,c2:?; v:?) (csubst0 (0) v c1 c2) ->
                             (c:?) (clear c1 c) -> (clear c2 c).
      Proof.
      XElim c1; Intros; CSubst0GenBase; Subst;
      (NewInduction k; Simpl in H3; [ XInv | Subst; ClearGenBase; XDEAuto 3]).
      Qed.

      Lemma csubst0_clear_O_back: (c1,c2:?; v:?) (csubst0 (0) v c1 c2) ->
                                  (c:?) (clear c2 c) -> (clear c1 c).
      Proof.
      XElim c1; Intros; CSubst0GenBase; Subst;
      (NewInduction k; Simpl in H3; [ XInv | Subst; ClearGenBase; XDEAuto 3]).
      Qed.

      Lemma csubst0_clear_S: (c1,c2:?; v:?; i:?) (csubst0 (S i) v c1 c2) ->
                             (c:?) (clear c1 c) -> (OR (clear c2 c) |
                             (EX b e u1 u2 | c = (CHead e (Bind b) u1) &
                                             (clear c2 (CHead e (Bind b) u2)) &
                                             (subst0 i v u1 u2)
                             ) |
                             (EX b e1 e2 u | c = (CHead e1 (Bind b) u) &
                                             (clear c2 (CHead e2 (Bind b) u)) &
                                             (csubst0 i v e1 e2)
                             ) |
                             (EX b e1 e2 u1 u2 | c = (CHead e1 (Bind b) u1) &
                                                 (clear c2 (CHead e2 (Bind b) u2)) &
                                                 (subst0 i v u1 u2) &
                                                 (csubst0 i v e1 e2)
                             )).
      Proof.
      XElim c1; Intros; CSubst0GenBase; Subst;
      NewInduction k; XInv; Subst; ClearGenBase.
(* case 1: csubst0_snd, bind *)
      XDEAuto 3.
(* case 2: csubst0_snd, flat *)
      XDEAuto 3.
(* case 3: csubst0_fst, bind *)
      XDEAuto 3.
(* case 4: csubst0_fst, flat *)
      LApply (H x0 v i); [ Clear H H3; Intros H | XAuto ].
      LApply (H c0); [ Clear H H1; Intros H | XAuto ].
      XDecompose H; XDEAuto 4.
(* case 5: csubst0_both, bind *)
      XDEAuto 3.
(* case 6: csubst0_both, flat *)
      LApply (H x1 v i); [ Clear H H3 H4; Intros H | XAuto ].
      LApply (H c0); [ Clear H H1; Intros H | XAuto ].
      XDecompose H; XDEAuto 4.
      Qed.

      Lemma csubst0_clear_trans: (c1,c2:?; v:?; i:?) (csubst0 i v c1 c2) ->
                                 (e2:?) (clear c2 e2) ->
                                 (clear c1 e2) \/
                                 (EX e1 | (csubst0 i v e1 e2) & (clear c1 e1)).
      Proof.
      XElim c1; Intros; CSubst0GenBase; Subst;
      NewInduction k; ClearGenBase.
(* case 1: csubst0_snd, bind *)
      XDEAuto 4.
(* case 2: csubst0_snd, flat *)
      XDEAuto 3.
(* case 3: csubst0_fst, bind *)
      XDEAuto 4.
(* case 4: csubst0_fst, flat *)
      XDecomPoseClear H '(H ? ? ? H5 ? H1); Clear H5 H1; XDEAuto 4.
(* case 5: csubst0_both, bind *)
      XDEAuto 4.
(* case 6: csubst0_both, flat *)
      XDecomPoseClear H '(H ? ? ? H6 ? H1); Clear H5 H6 H1; XDEAuto 4.
      Qed.

   End csubst0_clear.

      Tactic Definition CSubst0Clear := (
         Match Context With
            | [ H1: (csubst0 (0) ?1 ?2 ?3); H2: (clear ?2 ?4) |- ? ] ->
               LApply (csubst0_clear_O ?2 ?3 ?1); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ]
            | [ H1: (csubst0 (0) ?1 ?2 ?3); H2: (clear ?3 ?4) |- ? ] ->
               LApply (csubst0_clear_O_back ?2 ?3 ?1); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ]
            | [ H1: (csubst0 (S ?0) ?1 ?2 ?3); H2: (clear ?2 ?4) |- ? ] ->
               LApply (csubst0_clear_S ?2 ?3 ?1 ?0); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];
               XDecompose H1; Subst
            | [ H1: (csubst0 ? ? ? ?0); H2: (clear ?0 ?) |- ? ] ->
               XDecomPoseClear H2 '(csubst0_clear_trans ? ? ? ? H1 ? H2)
         ).

   Section csubst0_getl. (***************************************************)

      Hints Resolve csubst0_clear_O csubst0_clear_O_back : ld.

      Lemma csubst0_getl_ge: (i,n:?) (le i n) ->
                             (c1,c2:?; v:?) (csubst0 i v c1 c2) ->
                             (e:?) (getl n c1 e) -> (getl n c2 e).
      Proof.
      Intros; GetLGenBase.
      Apply (lt_eq_gt_e i n); Intros; Subst; [ Clear H | Clear H | Idtac ].
(* case 1: i < n *)
      CSubst0Drop; XDEAuto 2.
(* case 2: i = n *)
      CSubst0Drop; Subst; Try ClearGenBase; XDEAuto 4.
(* case 3: i > n *)
      LeLtGen.
      Qed.

      Lemma csubst0_getl_lt: (i,n:?) (lt n i) ->
                             (c1,c2:?; v:?) (csubst0 i v c1 c2) ->
                             (e:?) (getl n c1 e) -> (OR
                             (getl n c2 e) |
                             (EX b e0 u w | e = (CHead e0 (Bind b) u) &
                                            (getl n c2 (CHead e0 (Bind b) w)) &
                                            (subst0 (minus i (S n)) v u w)
                             ) |
                             (EX b e1 e2 u | e = (CHead e1 (Bind b) u) &
                                             (getl n c2 (CHead e2 (Bind b) u)) &
                                             (csubst0 (minus i (S n)) v e1 e2)
                             ) |
                             (EX b e1 e2 u w | e = (CHead e1 (Bind b) u) &
                                               (getl n c2 (CHead e2 (Bind b) w)) &
                                               (subst0 (minus i (S n)) v u w) &
                                               (csubst0 (minus i (S n)) v e1 e2)
                             )).
      Proof.
      Intros; GetLGenBase; CSubst0Drop; Subst.
(* case 1: none *)
      XDEAuto 3.
(* case 2: csubst0_snd *)
      NewInduction x0; ClearGenBase; XDEAuto 4.
(* case 3: csubst0_fst *)
      NewInduction x0; ClearGenBase; [ XDEAuto 4 | Clear H0; Simpl in H5  ].
      Rewrite minus_x_Sy in H5; [ Idtac | XAuto ].
      CSubst0Clear; XDEAuto 5.
(* case 4: csubst0_both *)
      NewInduction x0; ClearGenBase; [ XDEAuto 4 | Clear H0; Simpl in H5; Simpl in H6 ].
      Rewrite minus_x_Sy in H6; [ Idtac | XAuto ].
      CSubst0Clear; XDEAuto 5.
      Qed.

      Lemma csubst0_getl_ge_back: (i,n:?) (le i n) ->
                                  (c1,c2:?; v:?) (csubst0 i v c1 c2) ->
                                  (e:?) (getl n c2 e) -> (getl n c1 e).
      Proof.
      Intros; GetLGenBase.
      Apply (lt_eq_gt_e i n); Intros; Subst; [ Clear H | Clear H | Idtac ].
(* case 1: i < n *)
      CSubst0Drop; XDEAuto 2.
(* case 2: i = n *)
      CSubst0Drop; Subst; Try ClearGenBase; XDEAuto 4.
(* case 3: i > n *)
      LeLtGen.
      Qed.

      Lemma csubst0_getl_lt_back: (n,i:?) (lt n i) ->
                                  (c1,c2:?; v:?) (csubst0 i v c1 c2) ->
                                  (e2:?) (getl n c2 e2) ->
                                  (getl n c1 e2) \/
                                  (EX e1 | (csubst0 (minus i n) v e1 e2) &
                                           (getl n c1 e1)
                                  ).
      Proof.
      Intros; GetLGenBase; CSubst0Drop; Try CSubst0Clear; XDEAuto 4.
      Qed.

   End csubst0_getl.

      Tactic Definition CSubst0GetLTrans := (
         Match Context With
            | [H2: (csubst0 ?1 ?3 ?4 ?5); H3: (getl ?1 ?5 ?6) |- ? ] ->
               LApply (csubst0_getl_ge_back ?1 ?1); [ Intros H_x | XAuto ];
               LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
               LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ]
            | [ H1: (lt ?2 ?1);
                H2: (csubst0 ?1 ? ? ?0); H3: (getl ?2 ?0 ?) |- ? ] ->
               XDecomPoseClear H3 '(csubst0_getl_lt_back ? ? H1 ? ? ? H2 ? H3)
            | [H2: (csubst0 ?1 ?3 ?4 ?5); H3: (getl ?2 ?5 ?6) |- ? ] ->
               LApply (csubst0_getl_ge_back ?1 ?2); [ Intros H_x | XAuto ];
               LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
               LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ]
         ).

      Tactic Definition CSubst0GetL := (
         Match Context With
            | [ H1: (lt ?2 ?1);
                H2: (csubst0 ?1 ?3 ?4 ?5); H3: (getl ?2 ?4 ?6) |- ? ] ->
               LApply (csubst0_getl_lt ?1 ?2); [ Intros H_x | XAuto ];
               LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
               LApply (H_x ?6); [ Clear H_x H3; Intros H3 | XAuto ];
               XDecompose H3
            | [ H1: (le ?1 ?2);
                H2: (csubst0 ?1 ?3 ?4 ?5); H3: (getl ?2 ?4 ?6) |- ? ] ->
               LApply (csubst0_getl_ge ?1 ?2); [ Intros H_x | XAuto ];
               LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
               LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ]
            | [H2: (csubst0 ?1 ?3 ?4 ?5); H3: (getl ?1 ?4 ?6) |- ? ] ->
               LApply (csubst0_getl_ge ?1 ?1); [ Intros H_x | XAuto ];
               LApply (H_x ?4 ?5 ?3); [ Clear H_x H2; Intros H2 | XAuto ];
               LApply (H2 ?6); [ Clear H2 H3; Intros | XAuto ]
            | [ |- ? ] -> CSubst0GetLTrans
         ).