proposition: Lemma nth_sub_sup : forall t T n e f, sub_in_env t T n e f -> forall v : nat, n <= v -> forall u, item _ u e (S v) -> item _ u f v.
proof: Proof. simple induction 1. intros. inversion_clear H1; auto with coc core arith datatypes. simple destruct v; intros. inversion_clear H2. inversion_clear H3; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList