RichText.v (9 lines):
	- line 253: (* TODO: Show that the result of transformation of two
	- line 269: + (* 6/24 TODO: *) case: (interval_cases_analysisP _ _ _ _ _) => //=; rewrite andbT //.
	- line 278: + (* 7/24 TODO: *) admit.
	- line 290: + (* 11/24 TODO *) admit.
	- line 291: + (* 12/24 TODO *) admit.
	- line 337: (* TODO: This lemma is true only for nonempty operations *)
	- line 537: (*TODO: Fix holes in the proof *)
	- line 596: (*TODO: Prove commutation *)
	- line 599: (*TODO: Restrict to nonempty operations