meta/src/main/java/org/arend/lib/pattern/PatternUtils.java (2 lines):
	- line 337: if (actualPattern.isAbsurd()) { // TODO: This is not needed if implemented properly; see TODO below
	- line 368: // TODO: We should return null here, but to do this we need to substitute previous patterns in type


meta/src/main/java/org/arend/lib/meta/equation/MonoidSolver.java (2 lines):
	- line 257: // TODO: get rid of this shit with flags
	- line 690: // TODO: create a proper util method somewhere else instead of this


meta/src/main/java/org/arend/lib/level/StdLevelProver.java (1 line):
	- line 77: // TODO: Sigma types, pi types, equality (i.e., rising level), heterogeneous path types, recursive data types, dependently typed constructors