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

Require subst1_defs.
Require subst1_lift.
Require pr0_subst1.
Require pr1_defs.

   Section pr1_props. (******************************************************)

      Hints Resolve pr1_sing : ld.

      Lemma pr1_eta: (w,u:?) let t = (THead (Bind Abst) w u) in
                     (v:?) (pr1 v w) ->
                     (pr1 (THead (Bind Abst) v
                           (THead (Flat Appl) (TLRef (0)) (lift (1) (0) t)))
                          t).
      Proof.
      Intros; Unfold t; Clear t.
      Rewrite lift_bind.
      LApply (subst1_lift_S u (0) (0)); [ Intros | XAuto ].
      Apply pr1_comp; [ XDEAuto 2 | Clear H].
      EApply pr1_sing; [ EApply pr0_beta; XDEAuto 2 | XDEAuto 5 ].
      Qed.

   End pr1_props.