* renamed ll1 → runiq_alt and proved using new case-distinction rule trivial_cases
* updated documentation
* trying to redo some proofs without depending on runiq_alt (to see which runiq definition suits better)