Int_term.v



Require Termes.

  Definition intt := nat->term.

  Definition
shift_intt : intt->term->intt :=
     [i:intt][t:term][n:nat]Cases n of
         O => t
       | (S k) => (i k)
       end.


  Fixpoint int_term [t:term]: intt->nat->term :=
    [I:intt][k:nat]Cases t of
       (Srt s) => (Srt s)
     | (Ref n) => Case (le_gt_dec k n) of
                    [_:(le k n)](lift k (I (minus n k)))
                    [_:(gt k n)](Ref n)
                  end
     | (Abs A t) => (Abs (int_term A I k) (int_term t I (S k)))
     | (App u v) => (App (int_term u I k) (int_term v I k))
     | (Prod A B) => (Prod (int_term A I k) (int_term B I (S k)))
     end.


  Lemma int_term_subst: (t:term)(it:intt)(k:nat)(x:term)
       (subst_rec x (int_term t it (S k)) k)=(int_term t (shift_intt it x) k).
Induction t;Simpl;Intros;Auto.
Elim (le_gt_dec (S k) n);Intros.
Elim (le_gt_dec k n);Intros.
(Rewrite -> simpl_subst;Auto).
(Replace (minus n k) with (S (minus n (S k)));Auto).
(Rewrite -> minus_Sn_m;Auto).

Elim le_not_gt with k n ;Auto.

Simpl.
Elim (lt_eq_lt_dec k n);Intros.
Elim y0;Intros.
Absurd (le n k);Auto.

Elim (le_gt_dec k n);Intros;Auto.
Elim y1.
Replace (minus k k) with O;Auto.

Inversion_clear y1 in y2.
Elim gt_antirefl with n ;Auto.

Elim (le_gt_dec k n);Intros;Auto.
Absurd (le k n);Auto.

Rewrite -> H;Rewrite -> H0;Auto.

Rewrite -> H;Rewrite -> H0;Auto.

Rewrite -> H;Rewrite -> H0;Auto.
Save.


13/02/97, 13:20