[STATEMENT]
lemma eqvt:
  shows "eqvt (substClosed weakBisim)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt (substClosed weakBisim)
[PROOF STEP]
by(rule eqvtSubstClosed[OF Weak_Late_Bisim.eqvt])