proposition: Lemma inv_typ_prop : forall e T, typ e (Srt prop) T -> conv T (Srt kind).
proof: Proof. intros. apply typ_inversion with e (Srt prop) T; simpl in |- *; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList