proposition: Lemma hat_t_tau k: τ • t k = t (S k).
proof: Proof. cbn; asimpl; cbn; simplify. rewrite <-!enc_app. now replace (k * n + n) with (n + k * n) by 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