proposition: Lemma it_up_spec X n (sigma: fin -> @exp X) x: it n up_exp_exp sigma x = if dec2 lt x n then var_exp x else ren_exp (plus n) (sigma (x - n)).
proof: Proof. induction n in x, sigma |-*; cbn. - asimpl; destruct dec2; [lia|]; now destruct x. - destruct x; cbn; destruct dec2; (intuition idtac); [lia| |]. all: unfold funcomp; erewrite IHn. all: destruct dec2; intuition idtac; try lia; now asimpl. Qed.
imports: List Arith Lia Morphisms Undecidability.HOU(calculus.terms)