proposition: Lemma typ_sort_Econv_Econv : forall (e : env) (V U : term) (r s : sort), typ e V (Srt s) -> typ e U (Srt r) -> Econv U V -> Econv (Srt s) (Srt r).
proof: Proof. intros. generalize (typ_is_nf e V (Srt s) H). generalize (typ_is_nf e U (Srt r) H0). intros (x, H2) (x0, H3); intuition. apply Etyp_NF_Econv_Econv with x0 x e e; eauto with ecoc. apply normal_Econv_NF_conv; auto with ecoc. apply trans_Econv_Econv with U; auto with ecoc. apply sym_Econv. apply trans_Econv_Econv with V; trivial. apply Ered_Econv; auto with ecoc. apply Ered_Econv; auto with ecoc. unfold not in |- *; unfold is_lam in |- *; intros (x1, (x2, H6)). rewrite H6 in H8. apply inv_Etyp_abs with e x1 x2 (Srt s); trivial. apply typ_Etyp; trivial. intros. elim (Econv_sort_prod s x1 T); auto with ecoc. apply typ_Etyp; trivial. apply typ_Etyp; trivial. Qed.
imports: Termes Conv Ered Types ETypes Conv_Dec Strong_Norm