proposition: Lemma cl_trunc : forall (n : nat) (e f : cls), TTrunc _ n e f -> forall t : term, cl_term (lift n t) e = cl_term t f.
proof: Proof. simple induction 1; intros. rewrite lift0; auto with coc core arith datatypes. elim H1. rewrite simpl_lift. unfold lift at 1 in |- *. simpl in |- *. elim cl_term_lift with x (lift k t) 0 e0 (TCs _ x e0); auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType