[STATEMENT]
lemma left_unique_rel_gpv [transfer_rule]:
  "\<lbrakk> left_unique A; left_unique B \<rbrakk> \<Longrightarrow> left_unique (rel_gpv A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>left_unique A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (rel_gpv A B)
[PROOF STEP]
unfolding left_unique_alt_def gpv.rel_conversep[symmetric] gpv.rel_compp[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A OO A\<inverse>\<inverse> \<le> (=); B OO B\<inverse>\<inverse> \<le> (=)\<rbrakk> \<Longrightarrow> rel_gpv (A OO A\<inverse>\<inverse>) (B OO B\<inverse>\<inverse>) \<le> (=)
[PROOF STEP]
by(subst gpv.rel_eq[symmetric])(rule gpv.rel_mono)