proposition: Lemma steps_u u p q k: σ p q • u = t k ::: (τ • u) -> exists l, u = lin (tab (fun i => t (i + k)) l) r.
proof: Proof. specialize (well_founded_ind (measure_wf lt_wf (@size_exp ag))) as ind. revert k. induction u as [u IH] using ind; intros k EQ. destruct (step_u _ _ _ EQ) as [H1|H1]. - subst. exists 0. reflexivity. - destruct H1 as [u' H1]. rewrite H1 in EQ. rewrite !Cons_subst in EQ. asimpl in EQ. eapply Cons_injective in EQ as [_ EQ]. eapply IH in EQ as [l]; [|subst u; hnf; cbn; lia]. exists (S l). rewrite tab_S, H1, H. simplify. unfold Cons. f_equal. f_equal. rewrite !tab_map_nats. eapply map_ext. intros. f_equal; lia. 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