[STATEMENT]
lemma ifT_cong:
  assumes "b = c" "c \<Longrightarrow> x = u" "\<not>c \<Longrightarrow> y = v"
  shows "Heap_Monad_Ext.if\<^sub>T \<langle>b\<rangle> x y = Heap_Monad_Ext.if\<^sub>T \<langle>c\<rangle> u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Heap_Monad_Ext.if\<^sub>T \<langle>b\<rangle> x y = Heap_Monad_Ext.if\<^sub>T \<langle>c\<rangle> u v
[PROOF STEP]
unfolding Heap_Monad_Ext.if\<^sub>T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>b\<rangle> \<bind> (\<lambda>b. if b then x else y) = \<langle>c\<rangle> \<bind> (\<lambda>b. if b then u else v)
[PROOF STEP]
unfolding return_bind
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if b then x else y) = (if c then u else v)
[PROOF STEP]
using if_cong[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>c \<Longrightarrow> c; \<not> c \<Longrightarrow> \<not> c\<rbrakk> \<Longrightarrow> (if b then x else y) = (if c then u else v)

goal (1 subgoal):
 1. (if b then x else y) = (if c then u else v)
[PROOF STEP]
.