proposition: Lemma Econv_eq : forall (e : env) (a Ta : term), Etyp e a Ta -> forall b Tb : term, Etyp e b Tb -> NF_Econv a b -> Econv Ta Tb -> a = b.
proof: Proof. simple induction 1; intros. inversion H2; trivial. inversion H2; trivial. inversion H3; trivial. inversion H7. rewrite <- H13 in H6. apply inv_Etyp_abs with e0 T' M' Tb; trivial. intros; cut (T = T'); intros. rewrite H19; cut (M = M'); intros. rewrite H20; trivial. apply H5 with T1; trivial. rewrite H19; trivial. apply inv_Econv_prod_r with T T'. apply trans_Econv_Econv with Tb; auto with ecoc. apply H1 with (Srt s0); trivial. apply normal_Econv_NF_conv; trivial. apply inv_Econv_prod_l with U T1. apply trans_Econv_Econv with Tb; auto with ecoc. cut (Econv T T'). intros; apply Etyp_NF_Econv_Econv with T T' e0 e0; auto with ecoc. unfold not, is_lam in |- *; intros (x, (x0, H20)). rewrite H20 in H0. apply inv_Etyp_abs with e0 x x0 (Srt s1); trivial. intros. elim (Econv_sort_prod s1 x T2); auto with ecoc. apply inv_Econv_prod_l with U T1. apply trans_Econv_Econv with Tb; auto with ecoc. inversion H5. rewrite <- H11 in H4. apply inv_Etyp_app with e0 M' N' Tb; trivial. intros; cut (u = M'). intros; cut (v = N'). intros; rewrite H16; rewrite H17; trivial. apply H1 with V0; trivial. apply inv_Econv_prod_l with Ur Ur0. apply Etyp_NF_Econv_Econv with u M' e0 e0; auto with ecoc. apply H3 with (Prod V0 Ur0); trivial. apply Etyp_NF_Econv_Econv with u M' e0 e0; auto with ecoc. inversion H5. rewrite <- H10 in H4. apply inv_Etyp_prod with e0 T' U' Tb; trivial. intros; cut (T = T'). intros; cut (U = U'). intros; rewrite H15; rewrite H16; trivial. apply H3 with (Srt s3); auto. rewrite H15; trivial. apply trans_Econv_Econv with Tb; auto with ecoc. apply H1 with (Srt s0); auto. apply Etyp_NF_Econv_Econv with T T' e0 e0; auto with ecoc. unfold not, is_lam in |- *; intros (x, (x0, H15)). rewrite H15 in H0. apply inv_Etyp_abs with e0 x x0 (Srt s1); trivial. intros. elim (Econv_sort_prod s1 x T1); auto with ecoc. apply H1 with Tb; trivial. apply trans_Econv_Econv with V; auto with ecoc. Qed.
imports: Termes Conv Ered Types ETypes Conv_Dec Strong_Norm