240     then have "(c \<leftrightarrow> x) \<bullet> ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) \<turnstile> t : T2)" by (rule permute_boolI)

   240     then have "(c \<leftrightarrow> x) \<bullet> ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) \<turnstile> t : T2)" by (rule permute_boolI)

   241     then have "(c, T1) # \<Gamma>2 \<turnstile> ((c \<leftrightarrow> x) \<bullet> t) : T2" using fc1

   241     then have "(c, T1) # \<Gamma>2 \<turnstile> ((c \<leftrightarrow> x) \<bullet> t) : T2" using fc1

   242       by (perm_simp) (simp add: flip_fresh_fresh ty_fresh)

   242       by (perm_simp) (simp add: flip_fresh_fresh ty_fresh)

   243     then show "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" using fc1 by auto

   243     then show "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" using fc1 by auto

   244   qed

   244   qed

   246 qed (auto) -- {* var and app cases, luckily, are automatic *}

   246 qed (auto) -- {* var and app cases, luckily, are automatic *}

   247 

   247 

   248 

   248 

   249 text {* 

   249 text {* 

   250   The remedy is to use again a stronger induction principle that

   250   The remedy is to use again a stronger induction principle that