[STATEMENT]
lemma asymp_equiv_transfer:
  assumes "f1 \<sim>[F] g1" "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"
  shows   "f2 \<sim>[F] g2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f2 \<sim>[F] g2
[PROOF STEP]
using assms(1) asymp_equiv_cong[OF assms(2,3)]
[PROOF STATE]
proof (prove)
using this:
f1 \<sim>[F] g1
(f1 \<sim>[F] g1) = (f2 \<sim>[F] g2)

goal (1 subgoal):
 1. f2 \<sim>[F] g2
[PROOF STEP]
by simp