proposition: Lemma nth_class_env : forall (t : term) (e f : env) (n : nat), item _ t e n -> trunc _ (S n) e f -> cl_term t (class_env f) = Tnth_def _ Trm (class_env e) n.
proof: Proof. simple induction 1; simpl in |- *; intros. inversion_clear H0. inversion_clear H1; auto with coc core arith datatypes. apply H1. inversion_clear H2; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType