proposition: Lemma Etyp_NF_Econv_Econv : forall M M' : term, NF_Econv M M' -> ~ is_lam M -> forall (e e' : env) (A B : term), equiv_env Econv e e' -> Etyp e M A -> Etyp e' M' B -> Econv A B.
proof: Proof. simple induction 1; intros. apply inv_Etyp_ref with e A n; trivial; intros. apply inv_Etyp_ref with e' B n; trivial; intros. apply trans_Econv_Econv with (lift (S n) U); trivial. apply trans_Econv_Econv with (lift (S n) U0); auto with ecoc. unfold lift in |- *; apply Econv_Econv_lift. apply equiv_env_item with n e e'; trivial. apply inv_Etyp_app with e M0 N A; trivial. intros. apply inv_Etyp_app with e' M'0 N' B; trivial. intros. apply trans_Econv_Econv with (subst N Ur); trivial. apply sym_Econv; apply trans_Econv_Econv with (subst N' Ur0); trivial. unfold subst in |- *; apply Econv_Econv_subst. apply sym_Econv; apply NF_Econv_Econv; trivial. cut (Econv (Prod V Ur) (Prod V0 Ur0)). intros. apply sym_Econv. eapply inv_Econv_prod_r; eauto. apply H1 with e e'; trivial. elim H4; unfold is_lam in |- *; split with T; split with M0; trivial. generalize H2 H3; clear H2 H3; case s; intros. elim (inv_Etyp_kind e A H2). apply trans_Econv_Econv with (Srt kind). eapply inv_Etyp_prop; eauto. apply sym_Econv; eapply inv_Etyp_prop; eauto. apply trans_Econv_Econv with (Srt kind). eapply inv_Etyp_set; eauto. apply sym_Econv; eapply inv_Etyp_set; eauto. apply inv_Etyp_prod with e T U A; trivial; intros. apply inv_Etyp_prod with e' T' U' B; trivial; intros. apply trans_Econv_Econv with (Srt s2); auto with ecoc. apply trans_Econv_Econv with (Srt s3); auto with ecoc. apply H3 with (T :: e) (T' :: e'); trivial. unfold not, is_lam in |- *; intros (x, (x0, H14)). rewrite H14 in H9. apply inv_Etyp_abs with (T :: e) x x0 (Srt s2); trivial. intros. elim (Econv_sort_prod s2 x T0); auto with ecoc. constructor; auto with ecoc. Qed.
imports: Termes Conv Ered Types ETypes Conv_Dec Strong_Norm