proposition: Lemma Etyp_typ : forall (e : env) (M t : term), Etyp e M t -> typ e M t.
proof: Proof. fix Etyp_typ 4. intros. case H. intros; apply type_prop. case H0. apply wf_nil. intros; apply wf_var with s. apply Etyp_typ; trivial. intros; apply type_set. case H0. apply wf_nil. intros; apply wf_var with s. apply Etyp_typ; trivial. intros; apply type_var. case H0. apply wf_nil. intros; apply wf_var with s. apply Etyp_typ; trivial. trivial. intros. apply type_abs with s1 s2. apply Etyp_typ; trivial. apply Etyp_typ; trivial. apply Etyp_typ; trivial. intros; apply type_app with V. apply Etyp_typ; trivial. apply Etyp_typ; trivial. intros. apply type_prod with s1. apply Etyp_typ; trivial. apply Etyp_typ; trivial. intros. generalize (Etyp_typ e0 t0 U H0); intros. generalize (Etyp_typ e0 V (Srt s) H2); intros. generalize (type_case e0 t0 U H3). intros [(x, H5)| H6]. apply type_conv with U s; trivial. apply EConv_Conv with e0 (Srt x) (Srt s); trivial. apply typ_sort_Econv_Econv with e0 U V; auto with ecoc. rewrite H6 in H1. elim (inv_Etyp_Econv_kind e0 V (Srt s)); auto with ecoc. Qed.
imports: Termes Conv Ered Types ETypes Conv_Dec Strong_Norm