Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Sets.Ensembles.
Require Export Coq.Lists.List.
Require Import Coq.omega.Omega.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Classes.RelationClasses.
Require Import Logic.lib.Bijection.
Require Import Logic.lib.Countable.
Require Import Logic.lib.Ensembles_ext.
Require Import Logic.lib.EnsemblesProperties.

Section Lindenbaum.

(* Goal: forall _ : @eq A a a0, inj_R A nat CA a0 n *)
(* Goal: iff (or (LindenbaumChain n a0) (and (inj_R A nat CA a0 n) (P (Union A (LindenbaumChain n) (Singleton A a0))))) (or (LindenbaumChain n a0) (@eq A a a0)) *)
Context {A: Type}
        (CA: Countable A)
        (init: Ensemble A)
        (P: Ensemble A -> Prop).

Fixpoint LindenbaumChain (n: nat): Ensemble A :=
  match n with
  | 0 => init
  | S n => fun a => LindenbaumChain n a \/ CA a n /\ P (Union _ (LindenbaumChain n) (Singleton _ a))
  end.

Definition LindenbaumConstruction: Ensemble A :=
  fun a => exists n, LindenbaumChain n a.

Lemma Lindenbaum_included_n_m: forall n m,
  n <= m ->
  Included _ (LindenbaumChain n) (LindenbaumChain m).
Proof.
(* Goal: forall (CA : Countable A) (init : Ensemble A) (_ : P init), Intersection (Ensemble A) cP1 cP2 (@LindenbaumConstruction A CA init P) *)
  intros.
(* Goal: @ex nat (fun n : nat => @Forall A (LindenbaumChain n) xs) *)
  induction H.
  + exact (fun x H => H).
  + refine (fun x H => _ (IHle x H)).
(* Goal: forall _ : Ensembles.In A (LindenbaumChain m) x, Ensembles.In A (LindenbaumChain (S m)) x *)
    clear.
(* Goal: forall _ : Ensembles.In A (LindenbaumChain m) x, Ensembles.In A (LindenbaumChain (S m)) x *)
    unfold Ensembles.In; intros; simpl.
(* Goal: or (LindenbaumChain m x) (and (inj_R A nat CA x m) (P (Union A (LindenbaumChain m) (Singleton A x)))) *)
    left.
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
    auto.
Qed.

Lemma Lindenbaum_included_n_omega: forall n,
  Included _ (LindenbaumChain n) LindenbaumConstruction.
Proof.
(* Goal: forall (CA : Countable A) (init : Ensemble A) (_ : P init), Intersection (Ensemble A) cP1 cP2 (@LindenbaumConstruction A CA init P) *)
  intros.
(* Goal: Included A (LindenbaumChain n) LindenbaumConstruction *)
  intros ? ?.
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
  exists n; auto.
Qed.

Lemma Lindenbaum_included:
  Included _ init LindenbaumConstruction.
Proof.
(* Goal: Included A init LindenbaumConstruction *)
  apply (Lindenbaum_included_n_omega 0).
Qed.

Lemma Lindenbaum_pointwise_finite_decided: forall a n,
  CA a n ->
  (LindenbaumChain (S n) a) <-> (LindenbaumConstruction a).
Proof.
(* Goal: forall (CA : Countable A) (init : Ensemble A) (_ : P init), Intersection (Ensemble A) cP1 cP2 (@LindenbaumConstruction A CA init P) *)
  intros.
(* Goal: iff (LindenbaumChain (S n) a) (LindenbaumConstruction a) *)
  split; [apply (Lindenbaum_included_n_omega (S n)) | intros].
(* Goal: LindenbaumChain (S n) a *)
  destruct H0 as [m ?].
(* Goal: LindenbaumChain (S n) a *)
  destruct (le_dec m (S n)); [revert H0; apply Lindenbaum_included_n_m; auto |].
(* Goal: LindenbaumChain (S n) a *)
  assert (S n <= m) by omega; clear n0.
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
  induction H1; auto.
(* Goal: LindenbaumChain (S n) a *)
  apply IHle; clear IHle.
(* Goal: LindenbaumChain m a *)
  simpl in H0.
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
  destruct H0; auto.
(* Goal: LindenbaumChain m a *)
  destruct H0 as [? _]; exfalso.
(* Goal: False *)
  pose proof pf_inj _ _ CA a _ _ H H0.
(* Goal: False *)
  omega.
Qed.

Lemma Lindenbaum_finite_witness:
  forall xs, Forall LindenbaumConstruction xs ->
    exists n, Forall (LindenbaumChain n) xs.
Proof.
(* Goal: forall (CA : Countable A) (init : Ensemble A) (_ : P init), Intersection (Ensemble A) cP1 cP2 (@LindenbaumConstruction A CA init P) *)
  intros.
(* Goal: @ex nat (fun n : nat => @Forall A (LindenbaumChain n) xs) *)
  induction H.
  + exists 0.
(* Goal: @Forall A (LindenbaumChain (Init.Nat.max n (S m))) (@cons A x l) *)
    constructor.
  + destruct IHForall as [n ?H].
(* Goal: @ex nat (fun n : nat => @Forall A (LindenbaumChain n) (@cons A x l)) *)
    destruct (im_inj _ _ CA x) as [m ?].
(* Goal: @ex nat (fun n : nat => @Forall A (LindenbaumChain n) (@cons A x l)) *)
    exists (max n (S m)).
(* Goal: @Forall A (LindenbaumChain (Init.Nat.max n (S m))) (@cons A x l) *)
    constructor.
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
    - erewrite <- Lindenbaum_pointwise_finite_decided in H by eauto.
(* Goal: LindenbaumChain (Init.Nat.max n (S m)) x *)
      revert H; apply (Lindenbaum_included_n_m (S m)).
(* Goal: le (S m) (Init.Nat.max n (S m)) *)
      apply Max.le_max_r.
    - revert H1.
(* Goal: forall _ : @Forall A (LindenbaumChain n) l, @Forall A (LindenbaumChain (Init.Nat.max n (S m))) l *)
      apply Forall_impl; intro.
(* Goal: forall _ : LindenbaumChain n a, LindenbaumChain (Init.Nat.max n (S m)) a *)
      apply Lindenbaum_included_n_m.
(* Goal: le n (Init.Nat.max n (S m)) *)
      apply Max.le_max_l.
Qed.

Hypothesis H_init: P init.

Lemma Lindenbaum_preserve_n:
  Proper (Same_set A ==> iff) P ->
  forall n, P (LindenbaumChain n).
Proof.
(* Goal: forall (_ : @Proper (forall _ : Ensemble A, Prop) (@respectful (Ensemble A) Prop (Same_set A) iff) P) (n : nat), P (LindenbaumChain n) *)
  intros P_Proper n.
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
  induction n; auto.
(* Goal: iff (P (Union A (LindenbaumChain n) (Singleton A a))) (LindenbaumChain (S n) a) *)
  simpl.
(* Goal: P (fun a : A => or (LindenbaumChain n a) (and (inj_R A nat CA a n) (P (Union A (LindenbaumChain n) (Singleton A a))))) *)
  destruct (classic (exists a, CA a n /\ P (Union A (LindenbaumChain n) (Singleton A a)))).
  + destruct H as [a [? ?]].
(* Goal: P (fun a : A => or (LindenbaumChain n a) (and (inj_R A nat CA a n) (P (Union A (LindenbaumChain n) (Singleton A a))))) *)
    eapply P_Proper; [| exact H0].
(* Goal: Same_set A (fun a : A => or (LindenbaumChain n a) (and (inj_R A nat CA a n) (P (Union A (LindenbaumChain n) (Singleton A a))))) (LindenbaumChain n) *)
    rewrite Same_set_spec.
(* Goal: @pointwise_relation A Prop iff (fun a : A => or (LindenbaumChain n a) (and (inj_R A nat CA a n) (P (Union A (LindenbaumChain n) (Singleton A a))))) (LindenbaumChain n) *)
    intros a0.
(* Goal: iff (or (LindenbaumChain n a0) (and (inj_R A nat CA a0 n) (P (Union A (LindenbaumChain n) (Singleton A a0))))) (Union A (LindenbaumChain n) (Singleton A a) a0) *)
    rewrite Union_spec, Singleton_spec.
    assert (CA a0 n -> a = a0).
(* Goal: forall _ : @eq A a a0, inj_R A nat CA a0 n *)
(* Goal: iff (or (LindenbaumChain n a0) (and (inj_R A nat CA a0 n) (P (Union A (LindenbaumChain n) (Singleton A a0))))) (or (LindenbaumChain n a0) (@eq A a a0)) *)
    {
(* Goal: forall (CA : Countable A) (init : Ensemble A) (_ : P init), Intersection (Ensemble A) cP1 cP2 (@LindenbaumConstruction A CA init P) *)
      intros.
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
      apply (in_inj _ _ CA a a0 n); auto.
    }
    assert (a = a0 -> P (Union A (LindenbaumChain n) (Singleton A a0))).
(* Goal: forall _ : @eq A a a0, inj_R A nat CA a0 n *)
(* Goal: iff (or (LindenbaumChain n a0) (and (inj_R A nat CA a0 n) (P (Union A (LindenbaumChain n) (Singleton A a0))))) (or (LindenbaumChain n a0) (@eq A a a0)) *)
    {
(* Goal: forall (CA : Countable A) (init : Ensemble A) (_ : P init), Intersection (Ensemble A) cP1 cP2 (@LindenbaumConstruction A CA init P) *)
      intros.
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
      subst; auto.
    }
    assert (a = a0 -> CA a0 n).
(* Goal: forall _ : @eq A a a0, inj_R A nat CA a0 n *)
(* Goal: iff (or (LindenbaumChain n a0) (and (inj_R A nat CA a0 n) (P (Union A (LindenbaumChain n) (Singleton A a0))))) (or (LindenbaumChain n a0) (@eq A a a0)) *)
    {
(* Goal: forall (CA : Countable A) (init : Ensemble A) (_ : P init), Intersection (Ensemble A) cP1 cP2 (@LindenbaumConstruction A CA init P) *)
      intros.
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
      subst; auto.
    }
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
    tauto.
  + eapply P_Proper; [| exact IHn].
(* Goal: Same_set A (fun a : A => or (LindenbaumChain n a) (and (inj_R A nat CA a n) (P (Union A (LindenbaumChain n) (Singleton A a))))) (LindenbaumChain n) *)
    rewrite Same_set_spec.
(* Goal: @pointwise_relation A Prop iff (fun a : A => or (LindenbaumChain n a) (and (inj_R A nat CA a n) (P (Union A (LindenbaumChain n) (Singleton A a))))) (LindenbaumChain n) *)
    intros a0.
(* Goal: iff (or (LindenbaumChain n a0) (and (inj_R A nat CA a0 n) (P (Union A (LindenbaumChain n) (Singleton A a0))))) (LindenbaumChain n a0) *)
    firstorder.
Qed.

Lemma Lindenbaum_preserve_omega:
  finite_captured P ->
  subset_preserved P ->
  P LindenbaumConstruction.
Proof.
(* Goal: forall (CA : Countable A) (init : Ensemble A) (_ : P init), Intersection (Ensemble A) cP1 cP2 (@LindenbaumConstruction A CA init P) *)
  intros.
(* Goal: P LindenbaumConstruction *)
  apply H.
(* Goal: forall (CA : Countable A) (init : Ensemble A) (_ : P init), Intersection (Ensemble A) cP1 cP2 (@LindenbaumConstruction A CA init P) *)
  intros.
(* Goal: P (fun x : A => @In A x xs) *)
  apply Lindenbaum_finite_witness in H1.
(* Goal: P (fun x : A => @In A x xs) *)
  destruct H1 as [n ?].
(* Goal: P (fun x : A => @In A x xs) *)
  rewrite Forall_forall in H1.
(* Goal: P (fun x : A => @In A x xs) *)
  eapply H0; [exact H1 |].
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
  apply Lindenbaum_preserve_n, subset_preserved_same_set_preserved; auto.
Qed.

Lemma Lindenbaum_pointwise_finite_decided': forall a n,
  CA a n ->
  Proper (Same_set A ==> iff) P ->
  P (Union _ (LindenbaumChain n) (Singleton _ a)) <-> (LindenbaumConstruction a).
Proof.
(* Goal: forall (CA : Countable A) (init : Ensemble A) (_ : P init), Intersection (Ensemble A) cP1 cP2 (@LindenbaumConstruction A CA init P) *)
  intros.
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
  rewrite <- Lindenbaum_pointwise_finite_decided by eauto.
(* Goal: iff (P (Union A (LindenbaumChain n) (Singleton A a))) (LindenbaumChain (S n) a) *)
  simpl.
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
  split; intros; auto.
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
  destruct H1 as [? | [? ?]]; auto.
(* Goal: P (Union A (LindenbaumChain n) (Singleton A a)) *)
  eapply H0; [| apply (Lindenbaum_preserve_n H0 n)].
(* Goal: @pointwise_relation A Prop iff (fun a : A => or (LindenbaumChain n a) (and (inj_R A nat CA a n) (P (Union A (LindenbaumChain n) (Singleton A a))))) (LindenbaumChain n) *)
  rewrite Same_set_spec; intros a0.
(* Goal: iff (Union A (LindenbaumChain n) (Singleton A a) a0) (LindenbaumChain n a0) *)
  rewrite Union_spec.
(* Goal: iff (or (LindenbaumChain n a0) (Singleton A a a0)) (LindenbaumChain n a0) *)
  split; intros; [| auto].
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
  destruct H2; auto.
(* Goal: LindenbaumChain n a0 *)
  inversion H2; subst.
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
  auto.
Qed.

End Lindenbaum.

Definition Lindenbaum_preserves {A: Type} (P: Ensemble A -> Prop): Prop :=
  forall (CA: Countable A) init, P init -> P (LindenbaumConstruction CA init P).

Definition Lindenbaum_ensures {A: Type} (P cP: Ensemble A -> Prop): Prop :=
  forall (CA: Countable A) init, P init -> cP (LindenbaumConstruction CA init P).

Definition Lindenbaum_constructable {A: Type} (P cP: Ensemble A -> Prop): Prop :=
  forall Phi, P Phi -> exists Psi: sig cP, Included _ Phi (proj1_sig Psi) /\ P (proj1_sig Psi).

Lemma Lindenbaum_constructable_Same_set {A: Type}: forall P Q cP: Ensemble A -> Prop,
  Same_set _ P Q ->
  (Lindenbaum_constructable P cP <-> Lindenbaum_constructable Q cP).
Proof.
(* Goal: forall (CA : Countable A) (init : Ensemble A) (_ : P init), Intersection (Ensemble A) cP1 cP2 (@LindenbaumConstruction A CA init P) *)
  intros.
(* Goal: iff (@Lindenbaum_constructable A P cP) (@Lindenbaum_constructable A Q cP) *)
  pose proof H.
(* Goal: iff (@Lindenbaum_constructable A P cP) (@Lindenbaum_constructable A Q cP) *)
  rewrite Same_set_spec in H.
(* Goal: iff (@Lindenbaum_constructable A P cP) (@Lindenbaum_constructable A Q cP) *)
  apply Morphisms_Prop.all_iff_morphism.
(* Goal: @pointwise_relation (Ensemble A) Prop iff (fun x : Ensemble A => forall _ : P x, @ex (@sig (Ensemble A) cP) (fun Psi : @sig (Ensemble A) cP => and (Included A x (@proj1_sig (Ensemble A) cP Psi)) (P (@proj1_sig (Ensemble A) cP Psi)))) (fun x : Ensemble A => forall _ : Q x, @ex (@sig (Ensemble A) cP) (fun Psi : @sig (Ensemble A) cP => and (Included A x (@proj1_sig (Ensemble A) cP Psi)) (Q (@proj1_sig (Ensemble A) cP Psi)))) *)
  intros Phi.
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
  apply Morphisms_Prop.iff_iff_iff_impl_morphism_obligation_1; auto.
(* Goal: iff (@ex (@sig (Ensemble A) cP) (fun Psi : @sig (Ensemble A) cP => and (Included A Phi (@proj1_sig (Ensemble A) cP Psi)) (P (@proj1_sig (Ensemble A) cP Psi)))) (@ex (@sig (Ensemble A) cP) (fun Psi : @sig (Ensemble A) cP => and (Included A Phi (@proj1_sig (Ensemble A) cP Psi)) (Q (@proj1_sig (Ensemble A) cP Psi)))) *)
  apply Morphisms_Prop.ex_iff_morphism.
(* Goal: @pointwise_relation (@sig (Ensemble A) cP) Prop iff (fun Psi : @sig (Ensemble A) cP => and (Included A Phi (@proj1_sig (Ensemble A) cP Psi)) (P (@proj1_sig (Ensemble A) cP Psi))) (fun Psi : @sig (Ensemble A) cP => and (Included A Phi (@proj1_sig (Ensemble A) cP Psi)) (Q (@proj1_sig (Ensemble A) cP Psi))) *)
  intros [Psi ?H].
(* Goal: iff (and (Included A Phi (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1)))) (and (Included A Phi (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1)))) *)
  apply Morphisms_Prop.and_iff_morphism; [tauto |].
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
  auto.
Qed.

Lemma Lindenbaum_constructable_suffice {A: Type} (P cP: Ensemble A -> Prop):
  Countable A ->
  Lindenbaum_preserves P ->
  Lindenbaum_ensures P cP ->
  Lindenbaum_constructable P cP.
Proof.
(* Goal: forall (CA : Countable A) (init : Ensemble A) (_ : P init), Intersection (Ensemble A) cP1 cP2 (@LindenbaumConstruction A CA init P) *)
  intros.
(* Goal: forall (CA : Countable A) (init : Ensemble A) (_ : P init), Intersection (Ensemble A) cP1 cP2 (@LindenbaumConstruction A CA init P) *)
  hnf; intros.
(* Goal: @ex (@sig (Ensemble A) cP) (fun Psi : @sig (Ensemble A) cP => and (Included A Phi (@proj1_sig (Ensemble A) cP Psi)) (P (@proj1_sig (Ensemble A) cP Psi))) *)
  specialize (H X _ H1).
(* Goal: @ex (@sig (Ensemble A) cP) (fun Psi : @sig (Ensemble A) cP => and (Included A Phi (@proj1_sig (Ensemble A) cP Psi)) (P (@proj1_sig (Ensemble A) cP Psi))) *)
  specialize (H0 X _ H1).
(* Goal: @ex (@sig (Ensemble A) cP) (fun Psi : @sig (Ensemble A) cP => and (Included A Phi (@proj1_sig (Ensemble A) cP Psi)) (P (@proj1_sig (Ensemble A) cP Psi))) *)
  exists (exist _ _ H0).
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
  split; auto.
(* Goal: Included A Phi (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP (@LindenbaumConstruction A X Phi P) H0)) *)
  apply Lindenbaum_included.
Qed.

Lemma Lindenbaum_preserves_by_finiteness {A: Type}: forall P: Ensemble A -> Prop,
  finite_captured P ->
  subset_preserved P ->
  Lindenbaum_preserves P.
Proof.
(* Goal: forall (CA : Countable A) (init : Ensemble A) (_ : P init), Intersection (Ensemble A) cP1 cP2 (@LindenbaumConstruction A CA init P) *)
  intros.
(* Goal: forall (CA : Countable A) (init : Ensemble A) (_ : P init), Intersection (Ensemble A) cP1 cP2 (@LindenbaumConstruction A CA init P) *)
  hnf; intros.
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
  apply Lindenbaum_preserve_omega; auto.
Qed.

Lemma Lindenbaum_ensures_by_conjunct {A: Type}: forall P cP1 cP2: Ensemble A -> Prop,
  Lindenbaum_ensures P cP1 ->
  Lindenbaum_ensures P cP2 ->
  Lindenbaum_ensures P (Intersection _ cP1 cP2).
Proof.
(* Goal: forall (CA : Countable A) (init : Ensemble A) (_ : P init), Intersection (Ensemble A) cP1 cP2 (@LindenbaumConstruction A CA init P) *)
  intros.
(* Goal: @Lindenbaum_ensures A P (Intersection (Ensemble A) cP1 cP2) *)
  hnf.
(* Goal: forall (CA : Countable A) (init : Ensemble A) (_ : P init), Intersection (Ensemble A) cP1 cP2 (@LindenbaumConstruction A CA init P) *)
  intros.
(* Goal: iff (P (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) (Q (@proj1_sig (Ensemble A) cP (@exist (Ensemble A) cP Psi H1))) *)
  rewrite Intersection_spec; auto.
Qed.

