proposition: Lemma recognize_subst: forall `{Var V, Traverse V V, Traverse V T}, @TraverseFunctorial V _ V _ -> @TraverseIdentifiesVar V _ _ -> @TraverseRelative V V _ -> @TraverseRelative V T _ -> forall traverse_, traverse_ = traverse -> forall v k2 k1 t, traverse_ (fun l x => subst_idx (lift l 0 v) (l + k2) x) k1 t = subst (lift k1 0 v) (k1 + k2) t.
proof: Proof. intros. subst. unfold subst, Subst_Traverse. eapply traverse_relative; [ | instantiate (1 := k1); omega ]. intros. f_equal. rewrite lift_lift_fuse by omega. reflexivity. omega. Qed.
imports: Dblib.DblibTactics