proposition: Lemma step_u u p q k: σ p q • u = t k ::: (τ • u) -> u = r \/ (exists u', u = t k ::: u').
proof: Proof. intros EQ. destruct u as [| | | t1 t3]; try discriminate; auto. - cbn in *. asimpl in EQ. destruct f as [|[|[]]]; try discriminate. now left. - destruct t1 as [[|[|[]]]| | | t1 t2]; cbn in *; try discriminate; auto. destruct t1 as [[|[|[]]]| [] | |]; cbn in *; try discriminate; auto. injection EQ as EQ1 EQ2. intros. asimpl in EQ1. eapply subst_t in EQ1; subst; auto. right. now (exists t3). Qed.
imports: List Lia Program.Program Undecidability.HOU(std.std axioms) RelationClasses Morphisms Init.Wf Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.goldfarb.encoding) FinFun Coq.Arith.Wf_nat