proposition: Theorem str_norm : forall e t T, typ e t T -> sn t.
proof: Proof. intros. cut (is_can PROP (int_typ T (def_intp e) PROP)); auto with coc core arith datatypes. simpl in |- *; intros. cut (int_typ T (def_intp e) PROP t). elim H0; auto with coc core arith datatypes. elim id_int_term with e t 0. apply int_sound with e; auto with coc core arith datatypes. apply def_adapt. apply typ_wf with t T; auto with coc core arith datatypes. apply int_typ_cr; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can Int_term Int_typ Int_stab