proposition: Lemma lift_k_lift_k k n m t : lift k n (lift k m t) = lift k (n + m) t.
proof: Proof. funelim (lift k m t); intros; simp lift; try rewrite H ; try rewrite H0; auto. destruct (Nat.compare_spec i k); try discriminate. subst. case_eq (Nat.compare (k + n) k); intro H; simp lift; try term. rewrite Nat.compare_lt_iff in H; term. rewrite Heq; simp lift; term. rewrite Heq. rewrite Nat.compare_gt_iff in Heq. simp lift. destruct (Nat.compare_spec (i + n) k); try discriminate; simp lift; term. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia