195 apply (auto)[5]

   195 apply (auto)[5]

   196 --"LAST GOAL"

   196 --"LAST GOAL"

   197 apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])

   197 apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])

   198 apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)")

   198 apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)")

   199 apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))")

   199 apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))")

   200 prefer 2

   201 prefer 2

   201 apply (simp add: eqvt_at_def subst_def)

   202 apply (simp add: eqvt_at_def subst_def)

   202 apply rule

   203 apply rule

   203 apply (subst test2)

   204 apply (subst test2)

   204 apply (simp add: subst_substs_sumC_def)

   205 apply (simp add: subst_substs_sumC_def)

   213 apply(cases rule: subst_substs_graph.cases)

   214 apply(cases rule: subst_substs_graph.cases)

   214 apply assumption

   215 apply assumption

   215 apply (rule_tac x="lookup \<theta> X" in exI)

   216 apply (rule_tac x="lookup \<theta> X" in exI)

   216 apply clarify

   217 apply clarify

   217 apply (rule the1_equality)

   218 apply (rule the1_equality)

   219 apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1))))

   220 apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1))))

   220                   (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI)

   221                   (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI)

   221 apply clarify

   222 apply clarify

   222 apply (rule the1_equality)

   223 apply (rule the1_equality)

   224 apply clarify

   225 apply clarify

   225 apply simp

   226 apply simp

   226 --"-"

   227 --"-"

   227 apply clarify

   228 apply clarify

   228   apply (frule supp_eqvt_at)

   229   apply (frule supp_eqvt_at)