proposition: Lemma Etype_prop_set : forall s : sort, is_prop s -> forall e : env, Ewf e -> Etyp e (Srt s) (Srt kind).
proof: Proof. simple destruct 1; intros; rewrite H0. apply Etype_prop; trivial. apply Etype_set; trivial. Qed.
imports: Termes Conv Ered MyList Types