proposition: Lemma class_env_trunc : forall (k : nat) (e f : env), trunc _ k e f -> TTrunc _ k (class_env e) (class_env f).
proof: Proof. simple induction 1; simpl in |- *; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType