proposition: Lemma typ_is_nf : forall (e : env) (a Ta : term), typ e a Ta -> exists a' : term, red a a' /\ normal a' /\ typ e a' Ta.
proof: Proof. intros. elim (compute_nf a). intros; split with x; intuition; trivial. apply subject_reduction with a; trivial. apply str_norm with e Ta; trivial. Qed.
imports: Termes Conv Ered Types ETypes Conv_Dec Strong_Norm