proposition: Lemma nth_lift_int : forall (y : Int_K) (s0 : skel) (ipe ipf : intP) (n k : nat), TIns _ y k ipe ipf -> int_typ (lift_rec 1 (Ref n) k) ipf s0 = int_typ (Ref n) ipe s0.
proof: Proof. simpl in |- *; intros. elim (le_gt_dec k n). generalize n. elim H; simpl in |- *; auto with coc core arith datatypes. simple destruct n1; intro Hle; auto with coc core arith datatypes. inversion_clear Hle. generalize n. elim H; simpl in |- *; auto with coc core arith datatypes. intros l n0 Hgt. inversion_clear Hgt. simple destruct n1; intros; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can Int_typ