proposition: Lemma inductive_invariant:∀ m, m≤ n ⇒ ∃B', B'⊆town ∧ |B'| = m ∧ ∀ b'₀ b'₁, b'₀∈B' ⇒ b'₁∈B' ⇒ ¬(b'₀≡b'₁) ⇒ b'₀ ℛ b'₁.
proof: Proof. intros m. induction m; intros H_le. exists ∅. repeat split. apply subset_empty. intros b'₀ b'₁ H0 H1; apply False_ind. elim (FM.empty_iff b'₀); intros H2 _; apply H2; assumption. assert (H_le0:=le_Sn_le _ _ H_le). destruct (IHm H_le0) as [B' [H3' [H1 H2]]]. rewrite <- H1 in H_le0. destruct (extendible_to_n B' H3' H_le0) as [B [HB1 [HB2 HB3]]]. destruct (property B HB3 HB1) as [d [Hd1 Hd2]]. exists ({d}∪ B'); repeat split. apply subset_add_3. apply diff_1 with B; assumption. apply subset_trans with B; assumption. rewrite <- H1. apply add_cardinal_2. intro Hd4. generalize (in_subset Hd4 HB2). apply diff_2 with town; assumption. intros b'₀ b'₁ H_b'₀ H_b'₁ H_neq. destruct ((proj1 (FM.add_iff B' d b'₀)) H_b'₀) as [H3|H3]. apply knows_sym; apply knows_extensional with d; trivial. destruct ((proj1 (FM.add_iff B' d b'₁)) H_b'₁) as [H4|H4]. apply False_ind; apply H_neq; rewrite <- H3; assumption. apply knows_sym. apply Hd2; apply in_subset with B'; trivial. destruct ((proj1 (FM.add_iff B' d b'₁)) H_b'₁) as [H4|H4]. apply knows_extensional with d; trivial. apply knows_sym. apply Hd2; apply in_subset with B'; trivial. apply H2; assumption. Qed.
imports: Arith Omega