Library Int_term





Require
 Import
 Termes.

Require
 Import
 IntMap.




  Definition
 intt := nat -> term.




  Fixpoint
 int_term_rec (t
 : term) (I
 : intt) (k
 : nat) {struct
 t
} : term :=

    match
 t
 with


    | Srt s
 => Srt s


    | Ref n
 =>

        match
 le_gt_dec k
 n
 with


        | left _
 => lift k
 (I
 (n
 - k
))

        | right _
 => Ref n


        end


    | Abs A
 t
 => Abs (int_term_rec A
 I
 k
) (int_term_rec t
 I
 (S k
))

    | App u
 v
 => App (int_term_rec u
 I
 k
) (int_term_rec v
 I
 k
)

    | Prod A
 B
 => Prod (int_term_rec A
 I
 k
) (int_term_rec B
 I
 (S k
))

    end
.




  Definition
 int_term t
 I
 := int_term_rec t
 I
 0.




  Lemma
 int_term_subst :

   forall
 t
 it
 k
 x
,

   subst_rec x
 (int_term_rec t
 it
 (S k
)) k
 = int_term_rec t
 (cons_map x
 it
) k
.

simple
 induction
 t
; intros
.

auto
 with
 coc
.

unfold
 int_term_rec
 in
 |- *.

elim
 (le_gt_dec (S k
) n
); intros
.

elim
 (le_gt_dec k
 n
); intros
.

rewrite
 simpl_subst; auto
 with
 arith
.

replace
 (n
 - k
) with
 (S (n
 - S k
)); auto
 with
 arith
.

rewrite
 minus_Sn_m; auto
 with
 arith
.




elim
 le_not_gt with
 k
 n
; auto
 with
 arith
.




simpl
 in
 |- *.

elim
 (lt_eq_lt_dec k
 n
); intros
.

elim
 a
; intros
.

absurd
 (n
 <= k
); auto
 with
 arith
.




elim
 (le_gt_dec k
 n
); intros
; auto
 with
 coc
.

elim
 b0
.

replace
 (k
 - k
) with
 0; auto
 with
 arith
.




inversion_clear
 b0
 in
 b1
.

elim
 gt_irrefl with
 n
; auto
 with
 arith
.




elim
 (le_gt_dec k
 n
); intros
; auto
 with
 coc
.

absurd
 (k
 <= n
); auto
 with
 arith
.




simpl
 in
 |- *; rewrite
 H
; rewrite
 H0
; auto
 with
 coc
.




simpl
 in
 |- *; rewrite
 H
; rewrite
 H0
; auto
 with
 coc
.




simpl
 in
 |- *; rewrite
 H
; rewrite
 H0
; auto
 with
 coc
.

Qed
.