equal
deleted
inserted
replaced
84 apply (rule a2) |
84 apply (rule a2) |
85 apply simp |
85 apply simp |
86 apply simp |
86 apply simp |
87 apply (rule allI) |
87 apply (rule allI) |
88 apply (rule allI) |
88 apply (rule allI) |
89 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> TySch.All fset t) \<sharp>* pa)") |
89 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> All fset t) \<sharp>* pa)") |
90 apply clarify |
90 apply clarify |
91 apply(rule_tac t="p \<bullet> TySch.All fset t" and |
91 apply(rule_tac t="p \<bullet> All fset t" and |
92 s="pa \<bullet> (p \<bullet> TySch.All fset t)" in subst) |
92 s="pa \<bullet> (p \<bullet> All fset t)" in subst) |
93 apply (rule supp_perm_eq) |
93 apply (rule supp_perm_eq) |
94 apply assumption |
94 apply assumption |
95 apply (simp only: t_tyS.perm) |
95 apply (simp only: t_tyS.perm) |
96 apply (rule a3) |
96 apply (rule a3) |
97 apply(erule_tac x="(pa + p)" in allE) |
97 apply(erule_tac x="(pa + p)" in allE) |