proposition: Lemma mem_sort_lift : forall t n k s, mem_sort s (lift_rec n t k) -> mem_sort s t.
proof: Proof. simple induction t; simpl in |- *; intros; auto with coc core arith sets. generalize H; elim (le_gt_dec k n); intros; auto with coc core arith sets. inversion_clear H0. inversion_clear H1. apply mem_abs_l; apply H with n k; auto with coc core arith sets. apply mem_abs_r; apply H0 with n (S k); auto with coc core arith sets. inversion_clear H1. apply mem_app_l; apply H with n k; auto with coc core arith sets. apply mem_app_r; apply H0 with n k; auto with coc core arith sets. inversion_clear H1. apply mem_prod_l; apply H with n k; auto with coc core arith sets. apply mem_prod_r; apply H0 with n (S k); auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations