proposition: Lemma step_length_eq (rs : Ssts) v w : step rs v w -> length v = length w.
proof: Proof. case => > _. by rewrite !app_length. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun