[STATEMENT]
lemma either_contains_arg2: "paths t' \<subseteq> paths (t \<oplus>\<oplus> t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paths t' \<subseteq> paths (t \<oplus>\<oplus> t')
[PROOF STEP]
by transfer fastforce