proposition: Lemma mem_sort2_subst : forall (b a : term) (n : nat) (s : sort), mem_sort2 s (subst_rec a b n) -> mem_sort2 s a \/ mem_sort2 s b.
proof: Proof. simple induction b; simpl in |- *; intros; auto with ecoc coc core arith sets. generalize H; elim (lt_eq_lt_dec n0 n); [ intro a0 | intro b0 ]. elim a0; intros. inversion_clear H0. left. apply mem_sort2_lift with n0 0; auto with ecoc coc core arith sets. intros. inversion_clear H0. inversion_clear H1. elim H0 with a (S n) s; auto with ecoc coc core arith sets. inversion_clear H1. elim H with a n s; auto with ecoc coc core arith sets. elim H0 with a n s; auto with ecoc coc core arith sets. inversion_clear H1. elim H with a n s; auto with ecoc coc core arith sets. elim H0 with a (S n) s; intros; auto with ecoc coc core arith sets. Qed.
imports: Termes Conv