[STATEMENT]
lemma inv2_param[param]: "(inv2,inv2)\<in>\<langle>Rk,Rv\<rangle>rbt_rel\<rightarrow>Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inv2, inv2) \<in> \<langle>Rk, Rv\<rangle>rbt_rel \<rightarrow> bool_rel
[PROOF STEP]
unfolding inv2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rec_rbt True (\<lambda>c lt k v rt lta rta. lta \<and> rta \<and> bheight lt = bheight rt), rec_rbt True (\<lambda>c lt k v rt lta rta. lta \<and> rta \<and> bheight lt = bheight rt)) \<in> \<langle>Rk, Rv\<rangle>rbt_rel \<rightarrow> bool_rel
[PROOF STEP]
by (parametricity)