proposition: Lemma it_up_lt X n (sigma: fin -> @exp X) x: x < n -> it n up_exp_exp sigma x = var_exp x.
proof: Proof. intros; rewrite it_up_spec; destruct dec2; intuition easy. Qed.
imports: List Arith Lia Morphisms Undecidability.HOU(calculus.terms)