proposition: Lemma typ_Etyp : forall (e : env) (a Ta : term), typ e a Ta -> Etyp e a Ta.
proof: Proof. fix typ_Etyp 4. intros. case H; intros. apply Etype_prop. case H0. apply Ewf_nil. intros; apply Ewf_var with s. apply typ_Etyp; trivial. apply Etype_set. case H0. apply Ewf_nil. intros; apply Ewf_var with s; auto. apply Etype_var. case H0. apply Ewf_nil. intros; apply Ewf_var with s. apply typ_Etyp; trivial. trivial. apply Etype_abs with s1 s2; auto. apply Etype_app with V; auto. apply Etype_prod with s1; auto. apply Etype_Econv with U s; auto. apply conv_Econv; trivial. Qed.
imports: Termes Conv Ered MyList Types