proposition: Lemma Ewf_sort : forall (n : nat) (e f : env), trunc _ (S n) e f -> Ewf e -> forall t : term, item _ t e n -> exists s : sort, Etyp f t (Srt s).
proof: Proof. simple induction n. do 3 intro. inversion_clear H. inversion_clear H0. intros. inversion_clear H0. inversion_clear H. exists s; auto with coc core arith datatypes. do 5 intro. inversion_clear H0. intros. inversion_clear H2. inversion_clear H0. elim H with e0 f t; intros; auto with coc core arith datatypes. exists x0; auto with coc core arith datatypes. apply Etyp_Ewf with x (Srt s); auto with coc core arith datatypes. Qed.
imports: Termes Conv Ered MyList Types