--- a/Quot/Nominal/LFex.thy	Mon Feb 01 11:16:31 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Mon Feb 01 11:39:59 2010 +0100
@@ -646,18 +646,24 @@
 apply (rule refl)
 prefer 2
 apply(simp add: eqvts supp_eqvt atom_eqvt)
-sorry
+sorry (* Stuck *)
 
 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abst {atom x} K)) \<union> supp A"
-apply (subst supp_Pair[symmetric])
+(*apply (subst supp_Pair[symmetric])*)
 unfolding supp_def
 apply (simp add: permute_set_eq)
 apply(subst abs_eq)
 apply(subst KIND_TY_TRM_INJECT)
 apply(simp only: supp_fv)
 apply simp
-apply (unfold supp_def)
-sorry
+apply (simp_all add: Collect_imp_eq Collect_neg_eq)
+apply(subst Set.Un_commute)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
+apply (rule refl)
+prefer 2
+apply (rule refl)
+sorry (* Stuck *)
 
 lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
 apply(subst supp_kpi_pre)
@@ -677,7 +683,8 @@
  "supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
 apply (simp_all only: supp_kind_ty_trm_easy)
 apply (simp add: supp_kpi)
-sorry
+sorry (* Other ones will follow similarily *)
+
 
 end