proposition: Lemma not_Ered_Abs_sort : forall (T M : term) (s : sort), ~ Ered (Abs T M) (Srt s).
proof: Proof. unfold not in |- *; intros. inversion H. generalize (inv_Ered_Abs T M P H0). intros (T', (U', H3)). rewrite H3 in H1; inversion H1. Qed.
imports: Termes Conv