proposition: Remark acquintance_1: forall B : t, Subset B town_1 -> cardinal B = 1 -> {d : elt |In d (diff town_1 B) /\ (forall b : elt, In b B -> familiarity_1 d b)}.
proof: Proof. intros B H_sub H_card. destruct (subsets_1 B H_sub H_card) as [[HB1|HB2]|HB3]. exists 2; split. rewrite HB1; apply mem_2; trivial. intro b; rewrite HB1; intro Hb. destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H]. compute in H; rewrite <- H; simpl; trivial. apply False_ind; apply (proj1 (FM.empty_iff b) H). exists 1; split. rewrite HB2; apply mem_2; trivial. intro b; rewrite HB2; intro Hb. destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H]. compute in H; rewrite <- H; simpl; trivial. apply False_ind; apply (proj1 (FM.empty_iff b) H). exists 2; split. rewrite HB3; apply mem_2; trivial. intro b; rewrite HB3; intro Hb. destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H]. compute in H; rewrite <- H; simpl; trivial. apply False_ind; apply (proj1 (FM.empty_iff b) H). Defined.
imports: AMM11262