- | /6 width=2 by frees_inv_append, lt_to_le, or3_intro1, and3_intro/
- | /5 width=1 by frees_append, lt_to_le, or3_intro2, and4_intro/
+ | /7 width=2 by frees_inv_append, yle_inj, lt_to_le, or3_intro1, and3_intro/
+ | /6 width=1 by frees_append, yle_inj, lt_to_le, or3_intro2, and4_intro/