proposition: Lemma normal_lift {t k n} : normal t → normal (lift k n t) with neutral_lift {t k n} : neutral t -> neutral (lift k n t).
proof: Proof. destruct 1; simp lift; constructor; term. destruct 1; simp lift; try (constructor; term). destruct Nat.compare; term. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia Relations Setoid