--- a/Sectxt_prop.thy	Wed Nov 20 18:51:51 2013 +0800
+++ b/Sectxt_prop.thy	Wed Nov 20 21:33:56 2013 +0800
@@ -39,6 +39,8 @@
     apply (case_tac e)
     apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits
                 dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 simp:alive_simps)
+    apply (frule_tac p = nat1 in file_fds_subset_pfds)
+    apply (rule a1, auto)
     done
 qed
 
@@ -77,6 +79,8 @@
     apply (case_tac e)
     apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits
                 dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 simp:alive_simps)
+    apply (frule_tac p = nat1 in file_fds_subset_pfds)
+    apply (rule a1, auto)
     done
 qed