proposition: Lemma mem_sort2_lift : forall (t : term) (n k : nat) (s : sort), mem_sort2 s (lift_rec n t k) -> mem_sort2 s t.
proof: Proof. simple induction t; simpl in |- *; intros; auto with ecoc coc core arith sets. generalize H; elim (le_gt_dec k n); intros; auto with ecoc coc core arith sets. inversion_clear H0. inversion_clear H1. apply mem_abs_r2; apply H0 with n (S k); auto with ecoc coc core arith sets. inversion_clear H1. apply mem_app_l2; apply H with n k; auto with ecoc coc core arith sets. apply mem_app_r2; apply H0 with n k; auto with ecoc coc core arith sets. inversion_clear H1. apply mem_prod_l2; apply H with n k; auto with ecoc coc core arith sets. apply mem_prod_r2; apply H0 with n (S k); auto with ecoc coc core arith sets. Qed.
imports: Termes Conv