[STATEMENT]
lemma Act\<^sub>\<alpha>_eq_iff: "Act\<^sub>\<alpha> \<alpha>1 t1 = Act\<^sub>\<alpha> \<alpha>2 t2 \<longleftrightarrow> tAct \<alpha>1 (rep_Tree\<^sub>\<alpha> t1) =\<^sub>\<alpha> tAct \<alpha>2 (rep_Tree\<^sub>\<alpha> t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Act\<^sub>\<alpha> \<alpha>1 t1 = Act\<^sub>\<alpha> \<alpha>2 t2) = (tAct \<alpha>1 (rep_Tree\<^sub>\<alpha> t1) =\<^sub>\<alpha> tAct \<alpha>2 (rep_Tree\<^sub>\<alpha> t2))
[PROOF STEP]
by (metis Act\<^sub>\<alpha>.abs_eq Tree\<^sub>\<alpha>.abs_eq_iff Tree\<^sub>\<alpha>_abs_rep)