proposition: Theorem AMM11262: {e:elt | In e town /\ forall u, In u town /\ ~(E.eq u e)-> knows e u}.
proof: Proof. destruct (inductive_invariant n (le_refl n)) as [B [HB1 [HB2 HB3]]]. destruct (property B HB1 HB2) as [d [Hd1 Hd2]]. set (C:=(diff town (d ++ B))). assert (H_susbset_C:Subset C town); [ subst C; apply subset_diff; apply subset_refl | ]. assert (H_inter_town: inter town (d ++ B)[=]d ++ B). rewrite inter_sym; apply inter_subset_equal; apply subset_add_3; trivial; apply diff_1 with B; assumption. assert (H_d_nin_B:~In d B); [apply diff_2 with town; assumption|]. assert (H_cardinal_C:cardinal C=n). assert (H_aux:cardinal (inter town (d ++ B))=S n). rewrite (@Equal_cardinal (inter town (d ++ B)) (d++B) H_inter_town); rewrite (add_cardinal_2 H_d_nin_B); rewrite HB2; reflexivity. generalize (diff_inter_cardinal town (d++B)); fold C; rewrite H_aux; rewrite cardinality; omega. destruct (property C H_susbset_C H_cardinal_C) as [e [He1 He2]]. exists e. assert (H_dB_town:Subset (d++B) town). intros a Ha0; destruct ((proj1 (FM.add_iff B d a)) Ha0) as [Had|HaB]. rewrite <- Had; apply diff_1 with B; assumption. apply HB1; assumption. assert (H_diff:diff town C [=] d++B ). unfold C; split; intro H_mem. assert (H_a0:=diff_1 H_mem); assert (H_a1:=diff_2 H_mem); destruct (In_dec a (d++B)) as [H_a2|H_a2]; trivial; apply False_ind; apply H_a1; exact (diff_3 H_a0 H_a2). destruct (In_dec a (diff town (d++B))) as [H_a2|H_a2]. apply False_ind; exact (diff_2 H_a2 H_mem). apply diff_3; trivial; apply H_dB_town; assumption. assert (H_e_dB:In e (d++B)); [rewrite <- H_diff; assumption|]. split. apply diff_1 with C; assumption... intros u [Hu Hu']. assert (H_town_part:town [=] (union C (d++B))). rewrite <- (diff_inter_all town (d++B)); rewrite H_inter_town; apply equal_refl. rewrite H_town_part in Hu. destruct (union_1 Hu) as [HuC|HudB]. apply He2; assumption. destruct ((proj1 (FM.add_iff B d u)) HudB) as [Hud|HuB]. apply knows_extensional with d; trivial. apply knows_sym. destruct ((proj1 (FM.add_iff B d e)) H_e_dB) as [Hed|HeB]. apply False_ind; apply Hu'; rewrite <- Hud; assumption. apply Hd2; assumption. destruct ((proj1 (FM.add_iff B d e)) H_e_dB) as [Hed|HeB]. apply knows_sym; apply knows_extensional with d; trivial; apply knows_sym; apply Hd2; assumption. apply HB3; assumption || contradict Hu'; auto with *. Qed.
imports: Arith Omega