proposition: Lemma inv_typ_applist_head : forall e t l T, typ e (applist l t) T -> exists U : _, typ e t U.
proof: Proof. simple induction l; simpl in |- *; intros. split with T; trivial. apply inv_typ_app with (1 := H0); intros. eauto. Qed.
imports: Termes Types Conv Conv_Dec Strong_Norm Lia