proposition: Lemma recognize_lift: forall `{Var V, Traverse V T}, TraverseRelative -> forall w k1 k2 t, forall traverse_, traverse_ = traverse -> traverse_ (fun l x => var (lift w (l + k2) x)) k1 t = lift w (k1 + k2) t.
proof: Proof. intros. subst. simpl. eapply traverse_relative; [ | instantiate (1 := k1); omega ]. just_do_it. Qed.
imports: Dblib.DblibTactics