proposition: Lemma tab_subst {X} sigma (f: nat -> exp X) n: sigma •₊ tab f n = tab (f >> subst_exp sigma) n.
proof: Proof. induction n; cbn; simplify; cbn; rewrite ?IHn; reflexivity. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)