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

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

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

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

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

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

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

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

   210   qed

   210   qed

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

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

   213 

   213 

   214 

   214 

   215 text {* 

   215 text {* 

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

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