take EmptyIns A ; :: thesis: EmptyIns A is absolutely-terminating
thus EmptyIns A is absolutely-terminating ; :: thesis: verum