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

Require iso_defs.
Require lift_gen.
Require drop1_defs.
Require getl_props.
Require pr2_gen.
Require pr3_props.
Require pr3_gen.
Require pr3_iso.
Require nf2_props.
Require nf2_dec.
Require sn3_defs.
Require sn3_gen.

   Section sn3_props. (******************************************************)

      Lemma sn3_cpr3_trans: (c:?; u1,u2:?) (pr3 c u1 u2) ->
                            (k:?; t:?) (sn3 (CHead c k u1) t) ->
                            (sn3 (CHead c k u2) t).
      Proof.
      Intros; XElim H0; Clear t; Intros.
(* single case: sn3_sing *)
      Apply sn3_sing; Intros.
      Apply H1; [ XAuto | EApply pr3_pr3_pr3_t; XDEAuto 2 ].
      Qed.

      Hints Resolve sn3_sing : ld.

      Theorem sn3_bind: (b:?; c:?; u:?) (sn3 c u) ->
                        (t:?) (sn3 (CHead c (Bind b) u) t) ->
                        (sn3 c (THead (Bind b) u t)).
      Proof.
      Intros until 1; XElim H; Clear u.
      Intros; Rename t1 into u; XElim H1; Clear t; Intros.
(* single case: sn3_sing *)
      EApply sn3_sing; Intros.
      XDecomPose '(bind_dec_not b Abst); Subst; Pr3Gen; Subst.
(* case 1: b = Abst, pr0_cong *)
      XDecomPose '(term_dec u x0); Subst.
(* case 1.1: u = x0 *)
      Clear H6; XDecomPose '(term_dec t1 x1); Subst;
      [ Apply H3; XAuto | XAuto ].
(* case 1.2: u <> x0 *)
      Clear H2 H3; XDecomPose '(term_dec t1 x1); Subst; (
         Apply H0; [ XAuto | XAuto | EApply sn3_cpr3_trans; XDEAuto 2 ]
      ).
(* case 2: b <> Abst, pr0_cong *)
      XDecomPose '(term_dec u x0); Subst.
(* case 2.1: u = x0 *)
      Clear H8; XDecomPose '(term_dec t1 x1); Subst;
      [ Apply H3; XAuto | XAuto ].
(* case 2.2: u <> x0 *)
      Clear H2 H3; XDecomPose '(term_dec t1 x1); Subst; (
         Apply H0; [ XAuto | XAuto | EApply sn3_cpr3_trans; XDEAuto 2 ]
      ).
(* case 3: b <> Abst, pr0_zeta *)
      Clear H H0 H2 H3.
      EApply sn3_gen_lift;
      [ EApply sn3_pr3_trans; [ Idtac | XDEAuto 2 ] | Idtac ]; XAuto.
      Qed.

      Theorem sn3_beta: (c:?; v,t:?)
                        (sn3 c (THead (Bind Abbr) v t)) ->
                        (w:?) (sn3 c w) ->
                        (sn3 c (THead (Flat Appl) v (THead (Bind Abst) w t))).
      Proof.
      Intros until 1; InsertEq H '(THead (Bind Abbr) v t); UnIntro H t; UnIntro H v.
      XElim H; Clear y; Intros; Subst; Rename x into v; Rename x0 into t.
      XElim H2; Clear w; Intros; Rename t1 into w.
(* single case: sn3_sing *)
      Apply sn3_pr2_intro; Intros.
      Pr2Gen; Subst.
(* case 1: pr0_cong *)
      Pr2Gen; Subst; XDecomPose '(term_dec w x2); Subst.
(* case 1.1: w = x2 *)
      Clear H5; XDecomPose '(term_dec v x0); Subst.
(* case 1.1.1: v = x0 *)
      Clear H7; XDecomPose '(term_dec t x3); Subst.
(* case 1.1.1.1: t = x3 *)
      Clear H6; Apply H3; XAuto.
(* case 1.1.1.2: t <> x3 *)
      Clear H H2 H3.
      EApply H0; [ Intros | Idtac | XAuto | XAuto ].
      XInv; Subst; Apply H4; XAuto.
      XAuto.
(* case 1.1.2: v <> x0 *)
      Clear H H2 H3; EApply H0; [ Intros | Idtac | XAuto | XAuto ].
      XInv; Subst; Apply H4; XAuto.
      XAuto.
(* case 1.2: w <> x2 *)
      Clear H H3; XDecomPose '(term_dec v x0); Subst.
(* case 1.2.1: v = x0 *)
      Clear H7; XDecomPose '(term_dec t x3); Subst.
(* case 1.2.1.1: t = x3 *)
      Clear H6; XAuto.
(* case 1.2.1.2: t <> x3 *)
      Clear H2; EApply H0; [ Intros | Idtac | XAuto | XAuto ].
      XInv; Subst; Apply H; XAuto.
      XAuto.
(* case 1.2.2: v <> x0 *)
      Clear H2; EApply H0; [ Intros | Idtac | XAuto | XAuto ].
      XInv; Subst; Apply H; XAuto.
      XAuto.
(* case 2: pr0_beta *)
      Clear H0 H1 H2 H3; XInv; Subst.
      XDecomPose '(term_dec v x2); Subst.
(* case 2.1: v = x2 *)
      Clear H8; XDecomPose '(term_dec t x3); Subst.
(* case 2.1.1: t = x3 *)
      Clear H9; XAuto.
(* case 1.2.1.2: t <> x3 *)
      Apply H; [ Intros; XInv; Subst; Apply H0; XAuto | XAuto ].
(* case 2.2: v <> x0 *)
      Apply H; [ Intros; XInv; Subst; Apply H0; XAuto | XAuto ].
(* case 3: pr0_upsilon *)
      Clear H H0 H1 H2 H3; XInv; Subst; EqFalse.
      Qed.

      Lemma sn3_appl_lref: (c:?; i:?) (nf2 c (TLRef i)) ->
                           (v:?) (sn3 c v) ->
                           (sn3 c (THead (Flat Appl) v (TLRef i))).
      Proof.
      Intros until 2; XElim H0; Clear v; Intros.
      Apply sn3_pr2_intro; Intros; Pr2Gen; Subst.
(* case 1: pr0_comp *)
      NF2Unfold; Subst.
      XDecomPose '(term_dec t1 x0); Subst;
      [ EApply H2; XAuto | XDEAuto 3 ].
(* case 2: pr0_beta *)
      XInv.
(* case 3: pr0_upsilon *)
      XInv.
      Qed.

      Lemma sn3_appl_abbr: (c,d:?; w:?; i:?)
                           (getl i c (CHead d (Bind Abbr) w)) -> (v:?)
                           (sn3 c (THead (Flat Appl) v (lift (S i) O w))) ->
                                  (sn3 c (THead (Flat Appl) v (TLRef i))).
      Proof.
      Intros; InsertEq H0 '(THead (Flat Appl) v (lift (S i) O w)); UnIntro H0 v.
      XElim H0; Clear y; Intros; Subst; Rename x into v.
(* single case: sn3_sing *)
      Apply sn3_pr2_intro; Intros.
      Pr2Gen; Subst.
(* case 1: pr0_cong *)
      Pr2Gen; Subst.
(* case 1.1: pr2_free *)
      XDecomPose '(term_dec v x0); Subst.
(* case 1.1.1: v = x0 *)
      Apply H2; XAuto.
(* case 1.1.2: v <> x0 *)
      Clear H2 H0; EApply H1; [ Idtac | Idtac | XAuto ].
      Intros; XInv; Subst; Apply H3; XAuto.
      XAuto.
(* case 1.2: pr2_delta *)
      Clear H2; GetLDis; XInv; Subst.
      XDecomPose '(term_dec v x0); Subst.
(* case 1.2.1: v = x0 *)
      XAuto.
(* case 1.2.2: v <> x0 *)
      Apply H0; [ Intros; XInv; Subst; Apply H2; XAuto | XDEAuto 3 ].
(* case 2: pr0_beta *)
      XInv.
(* case 3: pr0_upsilon *)
      XInv.
      Qed.

      Theorem sn3_appl_cast: (c:?; v,u:?) (sn3 c (THead (Flat Appl) v u)) ->
                             (t:?) (sn3 c (THead (Flat Appl) v t)) ->
                             (sn3 c (THead (Flat Appl) v (THead (Flat Cast) u t))).
      Proof.
      Intros until 1.
      InsertEq H '(THead (Flat Appl) v u); UnIntro H u; UnIntro H v.
      XElim H; Clear y; Intros; Rename x into v; Rename x0 into u.
      InsertEq H2 '(THead (Flat Appl) v t); UnIntro H2 t.
      XElim H2; Clear y; Intros; Rename x into t; Subst.
(* single case: sn3_sing. *)
      Apply sn3_pr2_intro; Intros.
      Pr2Gen; Subst.
(* case 1: pr0_cong *)
      Pr2Gen; Subst.
(* case 1.1: pr0_cong *)
      XDecomPose '(term_dec (THead (Flat Appl) v u) (THead (Flat Appl) x0 x2)).
(* case 1.1.1: v = x0 and u = x2 *)
      XInv; Subst; Clear H0 H2 H.
      XDecomPose '(term_dec (THead (Flat Appl) v t) (THead (Flat Appl) v x3)).
(* case 1.1.1.1: t = x3 *)
      XInv; Subst; EApply H1; XAuto.
(* case 1.1.2.2: t <> x3 *)
      XDEAuto 4.
(* case 1.1.2: v <> x0 or u <> x2 *)
      Clear H3 H H1.
      XDecomPose '(term_dec (THead (Flat Appl) v t) (THead (Flat Appl) x0 x3)).
(* case 1.1.2.1: v = x0 and t = x3 *)
      XInv; Subst; XDEAuto 5.
(* case 1.1.2.2: v <> x0 or t <> x3 *)
      EApply H0; XDEAuto 6.
(* case 1.2: pr0_cast *)
      XDecomPose '(term_dec (THead (Flat Appl) v t) (THead (Flat Appl) x0 x1));
      XInv; Subst; XDEAuto 6.
(* case 2: pr0_beta *)
      XInv.
(* case 3: pr0_upsilon *)
      XInv.
      Qed.

      Hint discr : ld := Extern 4 (drop ? ? ? ?) Simpl.

      Theorem sn3_appl_bind: (b:?) ~b=Abst -> (c:?; u:?) (sn3 c u) -> (t:?; v:?)
                             (sn3 (CHead c (Bind b) u) (THead (Flat Appl) (lift (S O) O v) t)) ->
                             (sn3 c (THead (Flat Appl) v (THead (Bind b) u t))).
      Proof.
      Intros until 2; XElim H0; Clear u.
      Intros; Rename t1 into u.
      InsertEq H2 '(THead (Flat Appl) (lift (S O) O v) t).
      UnIntro H2 t; UnIntro H2 v; XElim H2; Clear y.
      Intros; Rename x into v; Rename x0 into t; Subst.
(* single case: sn3_sing *)
      EApply sn3_pr2_intro; Intros.
      Pr2Gen; Subst.
(* case 1: pr0_cong *)
      Pr3Gen; Subst.
(* case 1.1: pr0_cong *)
      XDecomPose '(term_dec u x2); Subst.
(* case 1.1.1: u = x2 *)
      Clear H0 H1 H2 H7.
      XDecomPose '(term_dec t x3); Subst.
(* case 1.1.1.1: t = x3 *)
      XDecomPose '(term_dec v x0); Subst.
(* case 1.1.1.1.1: v = x0 *)
      Apply H4; XAuto.
(* case 1.1.1.1.2: v <> x0 *)
      Clear H4 H10.
      EApply H3; [ Idtac | Idtac | XAuto ]; [ Idtac | Apply pr3_flat; XDEAuto 4 ].
      Intros; XInv; LiftGen; Subst; Apply H0; XAuto.
(* case 1.1.1.2: t <> x3 *)
      EApply H3; [ Idtac | Idtac | XAuto ]; [ Idtac | Apply pr3_flat; XDEAuto 5 ].
      Intros; XInv; LiftGen; Subst; Apply H0; XAuto.
(* case 1.1.2: u <> x2 *)
      EApply H1; [ XAuto | XAuto | Idtac ].
      EApply sn3_cpr3_trans; [ XDEAuto 2 | Idtac ].
      Clear H0 H1 H3 H4.
      XDecomPose '(term_dec t x3); Subst.
(* case 1.1.2.1: t = x3 *)
      XDecomPose '(term_dec v x0); Subst.
(* case 1.1.2.1.1: v = x0 *)
      Clear H8 H10; XAuto.
(* case 1.1.2.1.2: v <> x0 *)
      Clear H10; Apply H2; [ Idtac | Apply pr3_flat; XDEAuto 4 ].
      Intros; XInv; LiftGen; Subst; Apply H0; XAuto.
(* case 1.1.2.2: t <> x3 *)
      Apply H2; [ Idtac | Apply pr3_flat; XDEAuto 4 ].
      Intros; XInv; LiftGen; Subst; Apply H0; XAuto.
(* case 1.2: pr0_zeta *)
      Clear H0 H1 H3 H4.
      EApply sn3_gen_lift with c1:=(CHead c (Bind b) u);
      [ LiftHeadRw; Simpl | XAuto ].
      EApply sn3_pr3_trans with t1:=(THead (Flat Appl) (lift (S O) O x0) t); [ Idtac | XAuto ].
      XDecomPose '(term_dec v x0); Subst.
(* case 1.2.1: v = x0 *)
      Clear H8; XAuto.
(* case 1.2.2: v <> x0 *)
      EApply H2; [ Idtac | Apply pr3_flat; XDEAuto 4 ].
      Intros; XInv; LiftGen; Subst; Apply H0; XAuto.
(* case 2: pr0_beta *)
      XInv; Subst; EqFalse.
(* case 3: pr0_upsilon *)
      Clear H1 H3 H4 H7; XInv; Subst.
      Apply sn3_pr3_trans with t1:=(THead (Bind b) u (THead (Flat Appl) (lift (S O) O x4) x3)); [ Idtac | XAuto ].
      Apply sn3_bind; [ XAuto | Idtac ].
      Clear H0; XDecomPose '(term_dec v x4); Subst.
(* case 3.1: v = x4 *)
      Clear H10.
      XDecomPose '(term_dec t x3); Subst.
(* case 3.1.1: t = x3 *)
      Clear H12; XAuto.
(* case 3.1.2: t <> x3 *)
      Apply H2; [ Intros; XInv; Subst; Apply H0; XAuto | Idtac ].
      EApply pr3_pr3_pr3_t; [ Idtac | XDEAuto 3 ].
      XAuto.
(* case 3.2: v <> x4 *)
      Apply H2; [ Intros; XInv; LiftGen; Subst; Apply H0; XAuto | Idtac ].
      EApply pr3_pr3_pr3_t; [ Idtac | Apply pr3_flat; XDEAuto 4 ].
      XAuto.
      Qed.

      Hints Resolve pr3_sing sn3_pr3_trans iso_trans : ld.

      Lemma nf2_sn3: (c:?; t:?) (sn3 c t) ->
                     (EX u | (pr3 c t u) & (nf2 c u)).
      Proof.
      Intros; XElim H; Clear t; Intros.
(* single case: sn3_sing *)
      XDecomPose '(nf2_dec c t1).
(* case 1: t1 is pr2-normal *)
      XDEAuto 2.
(* case 2: t1 is not pr2-normal *)
      XPoseClear H0 '(H0 ? H2).
      LApply H0; [ Clear H0; Intros | XAuto ].
      XDecompose H0; XDEAuto 3.
      Qed.

      Theorem sn3_appl_appl: (v1,t1:?) let u1 = (THead (Flat Appl) v1 t1) in
                             (c:?) (sn3 c u1) ->
                             (v2:?) (sn3 c v2) ->
                             ((u2:?) (pr3 c u1 u2) ->
                              ((iso u1 u2) -> (P:Prop) P) ->
                              (sn3 c (THead (Flat Appl) v2 u2))
                             ) ->
                             (sn3 c (THead (Flat Appl) v2 u1)).
      Proof.
      Intros until u1; Unfold u1; Clear u1; Intros until 1.
      InsertEq H '(THead (Flat Appl) v1 t1); UnIntro H t1; UnIntro H v1.
      XElim H; Clear y; Intros until 4.
      XElim H2; Clear v2; Intros; Subst.
      Rename t0 into v2; Rename x into v1; Rename x0 into t1.
(* single case: sn3_sing *)
      Apply sn3_pr2_intro; Intros; Rename t2 into u2.
      Pr2Gen; Subst; Rename x0 into v0; Rename x1 into t0.
(* case 1: pr0_cong *)
      Pr2Gen; Subst; Rename x0 into v3; Rename x1 into t3.
(* case 1.1: pr0_cong *)
      XDecomPose '(term_dec (THead (Flat Appl) v1 t1) (THead (Flat Appl) v3 t3)).
(* case 1.1.1: v1 = v3 and t1 = t3 *)
      XInv; Subst; Clear H7 H10 H0.
      XDecomPose '(term_dec v2 v0); Subst;
      [ EApply H1; XAuto | Apply H3; XDEAuto 5 ].
(* case 1.1.2: v1 <> v3 or t1 <> t3 *)
      EApply H0; [ XDEAuto 2 | XDEAuto 5 | XDEAuto 2 | XDEAuto 4 | Intros ].
      Clear H H0 H1 H2 H3 H5; EApply sn3_pr3_trans; [ Apply H4 | XDEAuto 3 ].
(* case 1.1.2.1: first conclusion *)
      Clear H4; XDEAuto 5.
(* case 1.1.2.2: second conclusion *)
      Clear H4; Intros; Apply H9; XDEAuto 2.
(* case 1.2: pr0_beta *)
      Clear H H0 H1 H2 H3; EApply sn3_pr3_trans; [ Apply H4 | XDEAuto 3 ].
(* case 1.2.1: first conclusion *)
      Clear H4 H8; EApply pr3_sing;
      [ Apply pr2_free; Apply pr0_beta; XAuto | XDEAuto 4 ].
(* case 1.2.2: second conclusion *)
      Intros; Inversion H. (**)
(* case 1.3: pr0_upsilon *)
      Clear H H0 H1 H2 H3; EApply sn3_pr3_trans; [ Apply H4 | XDEAuto 3 ].
(* case 1.3.1: first conclusion *)
      Clear H4 H8; EApply pr3_sing;
      [ Apply pr2_free; Apply pr0_upsilon; XAuto
      | Apply pr3_head_12; [ XAuto | Apply pr3_head_12; XDEAuto 4 ]
      ].
(* case 1.3.2: second conclusion *)
      Intros; Inversion H. (**)
(* case 2: pr0_beta *)
      XInv.
(* case 3: pr0_upsilon *)
      XInv.
      Qed.

      Hints Resolve sn3_beta pr3_iso_beta : ld.

      Theorem sn3_appl_beta: (c:?; u,v,t:?)
                             (sn3 c (THead (Flat Appl) u (THead (Bind Abbr) v t))) ->
                             (w:?) (sn3 c w) ->
                             (sn3 c (THead (Flat Appl) u (THead (Flat Appl) v (THead (Bind Abst) w t)))).
      Proof.
      Intros; SN3GenBase; EApply sn3_appl_appl; XDEAuto 4.
      Qed.

      Hints Resolve sn3_appl_appl : ld.

      Theorem sn3_appl_appls: (v1,t1:?; vs:?) let u1 = (THeads (Flat Appl) (TCons v1 vs) t1) in
                              (c:?) (sn3 c u1) ->
                              (v2:?) (sn3 c v2) ->
                              ((u2:?) (pr3 c u1 u2) ->
                               ((iso u1 u2) -> (P:Prop) P) ->
                               (sn3 c (THead (Flat Appl) v2 u2))
                              ) ->
                              (sn3 c (THead (Flat Appl) v2 u1)).
      Proof.
      Intros until u1; Unfold u1; Clear u1; Simpl; XAuto.
      Qed.

      Hints Resolve nf2_iso_appls_lref sn3_appl_lref : ld.

      Lemma sn3_appls_lref: (c:?; i:?) (nf2 c (TLRef i)) ->
                            (us:?) (sns3 c us) ->
                            (sn3 c (THeads (Flat Appl) us (TLRef i))).
      Proof.
      XElim us; Simpl.
(* case 1: nil *)
      XAuto.
(* case 2: cons *)
      XElim t0; Intros.
(* case 2.1: cons, nil *)
      XDecompose H1; Simpl; XAuto.
(* case 2.2: cons, cons *)
      XDecompose H2; Simpl in H1.
      EApply sn3_appl_appls; [ XAuto | XAuto | Intros; Apply H4; XDEAuto 2 ].
      Qed.

      Hints Resolve pr3_iso_appls_cast sn3_appl_cast : ld.

      Theorem sn3_appls_cast: (c:?; vs:?; u:?) (sn3 c (THeads (Flat Appl) vs u)) ->
                              (t:?) (sn3 c (THeads (Flat Appl) vs t)) ->
                              (sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))).
      Proof.
      XElim vs; Simpl.
(* case 1: nil *)
      XAuto.
(* case 2: cons *)
      XElim t0; Intros.
(* case 2.1: cons, nil *)
      Simpl; XAuto.
(* case 2.2: cons, cons *)
      SN3GenBase; Clear H3; Cut (sn3 c (THeads (Flat Appl) (TCons t0 t1) t2)); [ Clear H4; Intros | XAuto ].
      Move H1 after H3; SN3GenBase; Clear H1; Cut (sn3 c (THeads (Flat Appl) (TCons t0 t1) u)); [ Clear H5; Intros | XAuto ].
      EApply sn3_appl_appls; XDEAuto 4.
      Qed.

      Hints Resolve sn3_bind sn3_appl_bind : ld.

      Theorem sn3_appls_bind: (b:?) ~b=Abst -> (c:?; u:?) (sn3 c u) -> (vs:?; t:?)
                              (sn3 (CHead c (Bind b) u) (THeads (Flat Appl) (lifts (S O) O vs) t)) ->
                              (sn3 c (THeads (Flat Appl) vs (THead (Bind b) u t))).
      Proof.
      XElim vs; Simpl.
(* case 1: TNil *)
      XAuto.
(* case 2: TCons *)
      Intros v vs; XElim vs; Intros.
(* case 2.1: TNil *)
      Simpl; XAuto.
(* case 2.2: TCons *)
      SN3GenBase; SN3Gen; EApply sn3_appl_appls; [ XDEAuto 2 | XDEAuto 2 | Intros ].
      XPose H8 '(pr3_iso_appls_bind ? H ? ? ? ? ? H6 H7); Clear H6 H7.
      EApply sn3_pr3_trans; [ Idtac | Apply pr3_flat; XDEAuto 2 ].
      XAuto.
      Qed.

      Hints Resolve sn3_appl_beta : ld.

      Theorem sn3_appls_beta: (c:?; v,t:?; us:?)
                              (sn3 c (THeads (Flat Appl) us (THead (Bind Abbr) v t))) ->
                              (w:?) (sn3 c w) ->
                              (sn3 c (THeads (Flat Appl) us (THead (Flat Appl) v (THead (Bind Abst) w t)))).
      Proof.
      XElim us; Simpl.
(* case 1: TNil *)
      XAuto.
(* case 2: TCons *)
      Intros u us; XElim us; Intros.
(* case 2.1: TNil *)
      Simpl; XAuto.
(* case 2.2: TCons *)
      SN3GenBase; EApply sn3_appl_appls; [ XDEAuto 2 | XDEAuto 2 | Intros ].
      XPose H7 '(pr3_iso_appls_beta ? ? ? ? ? ? H5 H6); Clear H5 H6.
      EApply sn3_pr3_trans; [ Idtac | Apply pr3_thin_dx; XDEAuto 2 ].
      XAuto.
      Qed.

      Lemma sn3_lift: (d:?; t:?) (sn3 d t) ->
                      (c:?; h,i:?) (drop h i c d) -> (sn3 c (lift h i t)).
      Proof.
      Intros until 1; XElim H; Intros.
(* single case: sn3_sing *)
      Apply sn3_pr2_intro; Intros; Pr2Gen; Subst.
      EApply H0; [ Intros; Subst; EApply H2; XAuto | XAuto | XAuto ].
      Qed.

      Hints Resolve sn3_lift : ld.

      Lemma sn3_abbr: (c,d:?; v:?; i:?) (getl i c (CHead d (Bind Abbr) v)) ->
                      (sn3 d v) -> (sn3 c (TLRef i)).
      Proof.
      Intros; EApply sn3_pr2_intro; Intros.
      Pr2Gen; Subst.
(* case 1: pr2_free *)
      EApply H1; XAuto.
(* case 2: pr2_delta *)
      Clear H1; GetLDis; XInv; Subst; GetLDrop; XDEAuto 2.
      Qed.

      Hints Resolve pr3_iso_appls_abbr sn3_abbr sn3_appl_abbr : ld.

      Lemma sn3_appls_abbr: (c,d:?; w:?; i:?)
                            (getl i c (CHead d (Bind Abbr) w)) -> (vs:?)
                            (sn3 c (THeads (Flat Appl) vs (lift (S i) O w))) ->
                                   (sn3 c (THeads (Flat Appl) vs (TLRef i))).
      Proof.
      XElim vs; Simpl.
(* case 1: TNil *)
      Intros; GetLDrop; SN3Gen; XDEAuto 2.
(* case 2: TCons *)
      Intros v vs; XElim vs; Intros.
(* case 2.1: TNil *)
      Simpl; XDEAuto 2.
(* case 2.2: TCons *)
      SN3GenBase; EApply sn3_appl_appls; XDEAuto 4.
      Qed.

   End sn3_props.

      Hints Resolve sn3_appls_abbr sn3_appls_cast sn3_appls_beta
                    sn3_lift : ld.

   Section sns3_props. (*****************************************************)

      Lemma sns3_lifts: (c,d:?; h,i:?) (drop h i c d) ->
                        (ts:?) (sns3 d ts) -> (sns3 c (lifts h i ts)).
      Proof.
      XElim ts; Simpl; Intros.
(* case 1: nil *)
      XAuto.
(* case 2: cons *)
      XDecompose H1; XDEAuto 4.
      Qed.

      Hints Resolve sns3_lifts : ld.

      Lemma sns3_lifts1: (e:?; hds:?; c:?) (drop1 hds c e) ->
                         (ts:?) (sns3 e ts) -> (sns3 c (lifts1 hds ts)).
      Proof.
      XElim hds; Simpl; Intros.
(* case 1: nil *)
      Drop1GenBase; Rewrite lifts1_nil; XAuto.
(* case 2: cons *)
      Drop1GenBase; Rewrite lifts1_cons; XDEAuto 3.
      Qed.

   End sns3_props.

      Hints Resolve sns3_lifts sns3_lifts1 : ld.