proposition: Remark R23 : const_pathS (n+l) gamma beta -> {beta = delta}+{const_pathS (n + l) delta beta}.
proof: Proof. intro H; now apply const_pathS_inv_strong. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)