proposition: Lemma applist_assoc : forall t e e', applist (e ++ e') t = applist e (applist e' t).
proof: Proof. simple induction e; simpl in |- *; intros; auto. rewrite H; trivial. Qed.
imports: Termes Types Conv Conv_Dec Strong_Norm Lia