proposition: Lemma inv_Etyp_set : forall (e : env) (T : term), Etyp e (Srt set) T -> Econv T (Srt kind).
proof: Proof. intros. apply Etyp_inversion with e (Srt set) T; simpl in |- *; auto with coc ecoc core arith datatypes. Qed.
imports: Termes Conv Ered MyList Types