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

Require sn3_defs.
Require sn3_props.
Require pc3_props.
Require ty3_defs.
Require ty3_gen.
Require ty3_props.
Require ty3_sred.
Require ty3_arity_props.

   Section ty3_gen_nf2. (****************************************************)

      Hints Resolve pc3_pr3_conf ty3_conv ty3_sred_pr3 : ld.

      Lemma ty3_gen_appl_nf2: (g:?; c:?; w,v,x:?) (ty3 g c (THead (Flat Appl) w v) x) ->
                              (EX u t | (pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x) &
                                        (ty3 g c v (THead (Bind Abst) u t)) &
                                        (ty3 g c w u) &
                                        (nf2 c (THead (Bind Abst) u t))
                              ).
      Proof.
      Intros; Ty3GenBase.
      XDecomPose '(ty3_correct ? ? ? ? H0).
      XDecomPose '(ty3_correct ? ? ? ? H1).
      XPose H4 '(ty3_sn3 ? ? ? ? H2).
      XDecomPoseClear H4 '(nf2_sn3 ? ? H4).
      Pr3GenBase; Subst.
      Cut (pr3 c (THead (Bind Abst) x0 x1) (THead (Bind Abst) x5 x6)); [ Clear H8; Intros H8 | XDEAuto 3 ].
      Apply ex4_2_intro with x0:=x5 x1:=x6;
      [ XDEAuto 3 | XDEAuto 4 | XDEAuto 4 | XAuto ].
      Qed.

   End ty3_gen_nf2.

      Tactic Definition Ty3GenNF2 := (
         Match Context With
            | [ H: (ty3 ? ? (THead (Flat Appl) ? ?) ?) |- ? ] ->
               XDecomPoseClear H '(ty3_gen_appl_nf2 ? ? ? ? ? H);
               NF2GenBase
            | [ |- ? ] -> Ty3GenBase
         ).