proposition: Lemma type_sn : forall e t T, typ e t T -> sn T.
proof: Proof. intros. elim type_case with e t T; intros; auto with coc core arith datatypes. elim H0; intros. apply str_norm with e (Srt x); auto with coc core arith datatypes. rewrite H0. red in |- *; apply Acc_intro; intros. inversion_clear H1. Qed.
imports: Termes Conv Types Class Can Int_term Int_typ Int_stab