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

Require lift_props.
Require subst_defs.

   Section subst_props. (****************************************************)

      Lemma subst_subst0: (v,t1,t2:?; d:?) (subst0 d v t1 t2) ->
                          (subst d v t1) = (subst d v t2).
      Proof.
      Intros; XElim H; Clear d v t1 t2; Intros.
(* case 1: subst0_lref *)
      Rewrite subst_lref_eq; Arith0 i.
      Rewrite <- lift_free with e:=i; Try Rewrite subst_lift_SO; XAuto.
(* case 2: subst0_fst *)
      Repeat Rewrite subst_head; Rewrite H0; XAuto.
(* case 3: subst0_snd *)
      Repeat Rewrite subst_head; Rewrite H0; XAuto.
(* case 4: subst0_both *)
      Repeat Rewrite subst_head; Rewrite H0; Rewrite H2; XAuto.
      Qed.

   End subst_props.