proposition: Lemma str_ind_r `{laws} `{STR ≪ l} n m (x: X n n) (z: X m n): z⋅x ≦ z -> z⋅x^* ≦ z.
proof: Proof. destruct str_ind_r_ as [Hl|[Hl|?]]. 3: auto. - rewrite <-2ldv_spec. intro E. apply str_leq in E. rewrite E. apply str_ldv_. - intros. cnv_switch. rewrite cnvdot, cnvstr_. apply str_ind_l; cnv_switch; now rewrite cnvdot, 2cnv_invol. Qed.
imports: lattice