[STATEMENT]
lemma cong_subst_right:
    assumes "u \<sim> u'" and "t \<frown> u"
    shows "t \<frown> u'" and "t \\ u \<sim> t \\ u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<frown> u' &&& t \ u \<sim> t \ u'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t \<frown> u'
 2. t \ u \<sim> t \ u'
[PROOF STEP]
have 1: "t \<frown> u' \<and> t \\ u' \<frown> u \\ u' \<and>
                (t \\ u) \\ (u' \\ u) = (t \\ u') \\ (u \\ u')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<frown> u' \<and> t \ u' \<frown> u \ u' \<and> (t \ u) \ (u' \ u) = (t \ u') \ (u \ u')
[PROOF STEP]
using assms cube con_sym con_target cong_subst_left(1)
[PROOF STATE]
proof (prove)
using this:
u \<sim> u'
t \<frown> u
(?v \ ?t) \ (?u \ ?t) = (?v \ ?u) \ (?t \ ?u)
?t \<frown> ?u \<Longrightarrow> ?u \<frown> ?t
\<lbrakk>?t \<lesssim> ?u; ?u \<frown> ?v\<rbrakk> \<Longrightarrow> ?t \ ?u \<frown> ?v \ ?u
\<lbrakk>?t \<sim> ?t'; ?t \<frown> ?u\<rbrakk> \<Longrightarrow> ?t' \<frown> ?u

goal (1 subgoal):
 1. t \<frown> u' \<and> t \ u' \<frown> u \ u' \<and> (t \ u) \ (u' \ u) = (t \ u') \ (u \ u')
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
t \<frown> u' \<and> t \ u' \<frown> u \ u' \<and> (t \ u) \ (u' \ u) = (t \ u') \ (u \ u')

goal (2 subgoals):
 1. t \<frown> u'
 2. t \ u \<sim> t \ u'
[PROOF STEP]
show "t \<frown> u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<frown> u'
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
t \<frown> u' \<and> t \ u' \<frown> u \ u' \<and> (t \ u) \ (u' \ u) = (t \ u') \ (u \ u')

goal (1 subgoal):
 1. t \<frown> u'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t \<frown> u'

goal (1 subgoal):
 1. t \ u \<sim> t \ u'
[PROOF STEP]
show "t \\ u \<sim> t \\ u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \ u \<sim> t \ u'
[PROOF STEP]
by (metis 1 arr_resid_iff_con assms(1) cong_reflexive resid_arr_ide)
[PROOF STATE]
proof (state)
this:
t \ u \<sim> t \ u'

goal:
No subgoals!
[PROOF STEP]
qed