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