Let c be given.

Assume Hc: nat_p c.

Assume IHc: ∀n, nat_p n → ∀X, infinite X → ∀C : set → set, (∀Y ⊆ X, equip Y n → C Y ∈ c) → ∃H ⊆ X, ∃i ∈ c, infinite H ∧ ∀Y ⊆ H, equip Y n → C Y = i.

We will prove ∀n, nat_p n → ∀X, infinite X → ∀C : set → set, (∀Y ⊆ X, equip Y n → C Y ∈ ordsucc c) → ∃H ⊆ X, ∃i ∈ ordsucc c, infinite H ∧ ∀Y ⊆ H, equip Y n → C Y = i.

Apply nat_ind to the current goal.

Let X be given.

Assume HX: infinite X.

Let C be given.

Assume H1: ∀Y ⊆ X, equip Y 0 → C Y ∈ ordsucc c.

We will prove ∃H ⊆ X, ∃i ∈ ordsucc c, infinite H ∧ ∀Y ⊆ H, equip Y 0 → C Y = i.

We use X to witness the existential quantifier.

Apply andI to the current goal.

We will prove X ⊆ X.

An exact proof term for the current goal is Subq_ref X.

We use C 0 to witness the existential quantifier.

Apply andI to the current goal.

We will prove C 0 ∈ ordsucc c.

Apply H1 0 to the current goal.

We will prove 0 ⊆ X.

Apply Subq_Empty to the current goal.

We will prove equip 0 0.

Apply equip_ref to the current goal.

We will prove infinite X ∧ ∀Y ⊆ X, equip Y 0 → C Y = C 0.

Apply andI to the current goal.

An exact proof term for the current goal is HX.

Let Y be given.

Assume HY: Y ⊆ X.

Assume HY0: equip Y 0.

We will prove C Y = C 0.

Use f_equal.

We will prove Y = 0.

An exact proof term for the current goal is equip_0_Empty Y HY0.

Let n be given.

Assume Hn: nat_p n.

Assume IHn: ∀X, infinite X → ∀C : set → set, (∀Y ⊆ X, equip Y n → C Y ∈ ordsucc c) → ∃H ⊆ X, ∃i ∈ ordsucc c, infinite H ∧ ∀Y ⊆ H, equip Y n → C Y = i.

Let X be given.

Assume HX: infinite X.

Let C be given.

Assume H1: ∀Y ⊆ X, equip Y (ordsucc n) → C Y ∈ ordsucc c.

We will prove ∃H ⊆ X, ∃i ∈ ordsucc c, infinite H ∧ ∀Y ⊆ H, equip Y (ordsucc n) → C Y = i.

Apply dneg to the current goal.

Assume H2: ¬ ∃H ⊆ X, ∃i ∈ ordsucc c, infinite H ∧ ∀Y ⊆ H, equip Y (ordsucc n) → C Y = i.

We prove the intermediate claim L1: ∀X' ⊆ X, infinite X' → ∃X'' ⊆ X', ∃x ∈ X', x ∉ X'' ∧ infinite X'' ∧ ∀Y ⊆ X'', equip Y n → C (Y ∪ {x}) = c.

Let X' be given.

Assume HX'X: X' ⊆ X.

Assume HX': infinite X'.

Apply dneg to the current goal.

Assume H2': ¬ ∃X'' ⊆ X', ∃x ∈ X', x ∉ X'' ∧ infinite X'' ∧ ∀Y ⊆ X'', equip Y n → C (Y ∪ {x}) = c.

We prove the intermediate claim L1a: ∃x, x ∈ X'.

Apply dneg to the current goal.

Assume H3: ¬ ∃x, x ∈ X'.

We prove the intermediate claim L1a1: X' = 0.

Apply Empty_eq to the current goal.

Let x be given.

Assume Hx: x ∈ X'.

Apply H3 to the current goal.

We use x to witness the existential quantifier.

An exact proof term for the current goal is Hx.

Apply HX' to the current goal.

We will prove finite X'.

rewrite the current goal using L1a1 (from left to right).

An exact proof term for the current goal is finite_Empty.

Apply L1a to the current goal.

Let x be given.

Assume Hx: x ∈ X'.

We prove the intermediate claim LX'xinf: infinite (X' ∖ {x}).

Apply infinite_remove1 to the current goal.

An exact proof term for the current goal is HX'.

Set C' to be the term λY ⇒ C (Y ∪ {x}) of type set → set.

We prove the intermediate claim LC'Sc: ∀Y ⊆ X' ∖ {x}, equip Y n → C' Y ∈ ordsucc c.

Let Y be given.

Assume H3: Y ⊆ X' ∖ {x}.

Assume H4: equip Y n.

We will prove C (Y ∪ {x}) ∈ ordsucc c.

Apply H1 to the current goal.

We will prove Y ∪ {x} ⊆ X.

Apply binunion_Subq_min to the current goal.

We will prove Y ⊆ X.

Apply Subq_tra Y (X' ∖ {x}) X H3 to the current goal.

We will prove X' ∖ {x} ⊆ X.

Apply Subq_tra (X' ∖ {x}) X' X to the current goal.

Apply setminus_Subq to the current goal.

We will prove X' ⊆ X.

An exact proof term for the current goal is HX'X.

We will prove {x} ⊆ X.

Let y be given.

Assume Hy: y ∈ {x}.

rewrite the current goal using SingE x y Hy (from left to right).

We will prove x ∈ X.

Apply HX'X to the current goal.

An exact proof term for the current goal is Hx.

We will prove equip (Y ∪ {x}) (ordsucc n).

Apply equip_sym to the current goal.

Apply equip_adjoin_ordsucc to the current goal.

We will prove x ∉ Y.

Assume H5: x ∈ Y.

Apply setminusE2 X' {x} x (H3 x H5) to the current goal.

We will prove x ∈ {x}.

Apply SingI to the current goal.

We will prove equip n Y.

Apply equip_sym to the current goal.

An exact proof term for the current goal is H4.

We prove the intermediate claim L1b: ∀Z ⊆ X', infinite Z → ∃Z' ⊆ Z, ∃y ∈ Z, y ∉ Z' ∧ infinite Z' ∧ ∀Y ⊆ Z', equip Y n → C (Y ∪ {y}) ∈ c.

Apply dneg to the current goal.

Assume H3: ¬ ∀Z ⊆ X', infinite Z → ∃Z' ⊆ Z, ∃y ∈ Z, y ∉ Z' ∧ infinite Z' ∧ ∀Y ⊆ Z', equip Y n → C (Y ∪ {y}) ∈ c.

Apply IHn (X' ∖ {x}) LX'xinf C' LC'Sc to the current goal.

Let H' be given.

Assume H.

Apply H to the current goal.

Assume HH'X': H' ⊆ X' ∖ {x}.

Assume H.

Apply H to the current goal.

Let i be given.

Assume H.

Apply H to the current goal.

Assume Hi: i ∈ ordsucc c.

Assume H.

Apply H to the current goal.

Assume HH'inf: infinite H'.

Assume HH'hom: ∀Y ⊆ H', equip Y n → C (Y ∪ {x}) = i.

Apply ordsuccE c i Hi to the current goal.

Assume H4: i ∈ c.

Apply H3 to the current goal.

Let Z be given.

Assume HZX': Z ⊆ X'.

Assume HZ: infinite Z.

Apply dneg to the current goal.

Assume H5: ¬ ∃Z' ⊆ Z, ∃y ∈ Z, y ∉ Z' ∧ infinite Z' ∧ ∀Y ⊆ Z', equip Y n → C (Y ∪ {y}) ∈ c.

We prove the intermediate claim L1b1: ∃y, y ∈ Z.

Apply dneg to the current goal.

Assume H6: ¬ ∃y, y ∈ Z.

We prove the intermediate claim L1b1a: Z = 0.

Apply Empty_eq to the current goal.

Let y be given.

Assume Hy: y ∈ Z.

Apply H6 to the current goal.

We use y to witness the existential quantifier.

An exact proof term for the current goal is Hy.

Apply HZ to the current goal.

We will prove finite Z.

rewrite the current goal using L1b1a (from left to right).

An exact proof term for the current goal is finite_Empty.

Apply L1b1 to the current goal.

Let y be given.

Assume Hy: y ∈ Z.

We prove the intermediate claim LZyinf: infinite (Z ∖ {y}).

Apply infinite_remove1 to the current goal.

An exact proof term for the current goal is HZ.

We prove the intermediate claim LZyX': Z ∖ {y} ⊆ X'.

Apply Subq_tra (Z ∖ {y}) Z X' to the current goal.

Apply setminus_Subq to the current goal.

An exact proof term for the current goal is HZX'.

We prove the intermediate claim LZyX: Z ∖ {y} ⊆ X.

An exact proof term for the current goal is Subq_tra (Z ∖ {y}) X' X LZyX' HX'X.

Set C'' to be the term λY ⇒ C (Y ∪ {y}) of type set → set.

We prove the intermediate claim LC''Sc: ∀Y ⊆ Z ∖ {y}, equip Y n → C'' Y ∈ ordsucc c.

Let Y be given.

Assume H6: Y ⊆ Z ∖ {y}.

Assume H7: equip Y n.

We will prove C (Y ∪ {y}) ∈ ordsucc c.

Apply H1 to the current goal.

We will prove Y ∪ {y} ⊆ X.

Apply binunion_Subq_min to the current goal.

We will prove Y ⊆ X.

Apply Subq_tra Y (Z ∖ {y}) X H6 to the current goal.

We will prove Z ∖ {y} ⊆ X.

An exact proof term for the current goal is LZyX.

We will prove {y} ⊆ X.

Let z be given.

Assume Hz: z ∈ {y}.

rewrite the current goal using SingE y z Hz (from left to right).

We will prove y ∈ X.

Apply HX'X to the current goal.

We will prove y ∈ X'.

Apply HZX' to the current goal.

We will prove y ∈ Z.

An exact proof term for the current goal is Hy.

We will prove equip (Y ∪ {y}) (ordsucc n).

Apply equip_sym to the current goal.

Apply equip_adjoin_ordsucc to the current goal.

We will prove y ∉ Y.

Assume H8: y ∈ Y.

Apply setminusE2 Z {y} y (H6 y H8) to the current goal.

We will prove y ∈ {y}.

Apply SingI to the current goal.

We will prove equip n Y.

Apply equip_sym to the current goal.

An exact proof term for the current goal is H7.

Apply IHn (Z ∖ {y}) LZyinf C'' LC''Sc to the current goal.

Let H' be given.

Assume H.

Apply H to the current goal.

Assume HH'Zy: H' ⊆ Z ∖ {y}.

Assume H.

Apply H to the current goal.

Let i be given.

Assume H.

Apply H to the current goal.

Assume Hi: i ∈ ordsucc c.

Assume H.

Apply H to the current goal.

Assume HH'inf: infinite H'.

Assume HH'hom: ∀Y ⊆ H', equip Y n → C (Y ∪ {y}) = i.

Apply ordsuccE c i Hi to the current goal.

Assume H6: i ∈ c.

Apply H5 to the current goal.

We use H' to witness the existential quantifier.

Apply andI to the current goal.

We will prove H' ⊆ Z.

Apply Subq_tra H' (Z ∖ {y}) Z HH'Zy to the current goal.

Apply setminus_Subq to the current goal.

We will prove ∃y ∈ Z, y ∉ H' ∧ infinite H' ∧ ∀Y ⊆ H', equip Y n → C (Y ∪ {y}) ∈ c.

We use y to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hy.

Apply and3I to the current goal.

Assume H7: y ∈ H'.

Apply setminusE2 Z {y} y (HH'Zy y H7) to the current goal.

Apply SingI to the current goal.

An exact proof term for the current goal is HH'inf.

Let Y be given.

Assume H7: Y ⊆ H'.

Assume H8: equip Y n.

rewrite the current goal using HH'hom Y H7 H8 (from left to right).

We will prove i ∈ c.

An exact proof term for the current goal is H6.

Assume H6: i = c.

Apply H2' to the current goal.

We use H' to witness the existential quantifier.

Apply andI to the current goal.

We will prove H' ⊆ X'.

Apply Subq_tra H' (Z ∖ {y}) X' HH'Zy to the current goal.

We will prove Z ∖ {y} ⊆ X'.

An exact proof term for the current goal is LZyX'.

We use y to witness the existential quantifier.

Apply andI to the current goal.

We will prove y ∈ X'.

Apply HZX' to the current goal.

An exact proof term for the current goal is Hy.

Apply and3I to the current goal.

We will prove y ∉ H'.

Assume H7: y ∈ H'.

Apply setminusE2 Z {y} y (HH'Zy y H7) to the current goal.

Apply SingI to the current goal.

We will prove infinite H'.

An exact proof term for the current goal is HH'inf.

rewrite the current goal using H6 (from right to left).

An exact proof term for the current goal is HH'hom.

Assume H4: i = c.

Apply H2' to the current goal.

We use H' to witness the existential quantifier.

Apply andI to the current goal.

We will prove H' ⊆ X'.

Apply Subq_tra H' (X' ∖ {x}) X' HH'X' to the current goal.

We will prove X' ∖ {x} ⊆ X'.

Apply setminus_Subq to the current goal.

We use x to witness the existential quantifier.

Apply andI to the current goal.

We will prove x ∈ X'.

An exact proof term for the current goal is Hx.

Apply and3I to the current goal.

We will prove x ∉ H'.

Assume H5: x ∈ H'.

Apply setminusE2 X' {x} x (HH'X' x H5) to the current goal.

Apply SingI to the current goal.

We will prove infinite H'.

An exact proof term for the current goal is HH'inf.

rewrite the current goal using H4 (from right to left).

An exact proof term for the current goal is HH'hom.

Set f to be the term λZ ⇒ Eps_i (λZ' ⇒ Z' ⊆ Z ∧ ∃y ∈ Z, y ∉ Z' ∧ infinite Z' ∧ ∀Y ⊆ Z', equip Y n → C (Y ∪ {y}) ∈ c) of type set → set.

We prove the intermediate claim Lf1: ∀Z ⊆ X', infinite Z → f Z ⊆ Z ∧ ∃y ∈ Z, y ∉ f Z ∧ infinite (f Z) ∧ ∀Y ⊆ f Z, equip Y n → C (Y ∪ {y}) ∈ c.

Let Z be given.

Assume HZ1 HZ2.

An exact proof term for the current goal is Eps_i_ex (λZ' ⇒ Z' ⊆ Z ∧ ∃y ∈ Z, y ∉ Z' ∧ infinite Z' ∧ ∀Y ⊆ Z', equip Y n → C (Y ∪ {y}) ∈ c) (L1b Z HZ1 HZ2).

We prove the intermediate claim Lf1a: ∀Z ⊆ X', infinite Z → f Z ⊆ Z ∧ infinite (f Z).

Let Z be given.

Assume HZ1 HZ2.

Apply Lf1 Z HZ1 HZ2 to the current goal.

Assume H3: f Z ⊆ Z.

Assume H.

Apply H to the current goal.

Let y be given.

Assume H.

Apply H to the current goal.

Assume Hy: y ∈ Z.

Assume H.

Apply H to the current goal.

Assume H4: y ∉ f Z ∧ infinite (f Z).

Assume _.

Apply H4 to the current goal.

Assume _.

Assume H5: infinite (f Z).

Apply andI to the current goal.

An exact proof term for the current goal is H3.

An exact proof term for the current goal is H5.

Set g to be the term λZ ⇒ Eps_i (λy ⇒ y ∈ Z ∧ (y ∉ f Z ∧ ∀Y ⊆ f Z, equip Y n → C (Y ∪ {y}) ∈ c)) of type set → set.

We prove the intermediate claim Lg1: ∀Z ⊆ X', infinite Z → g Z ∈ Z ∧ (g Z ∉ f Z ∧ ∀Y ⊆ f Z, equip Y n → C (Y ∪ {g Z}) ∈ c).

Let Z be given.

Assume HZ1 HZ2.

Apply Lf1 Z HZ1 HZ2 to the current goal.

Assume H3: f Z ⊆ Z.

Assume H.

Apply H to the current goal.

Let y be given.

Assume H.

Apply H to the current goal.

Assume Hy: y ∈ Z.

Assume H.

Apply H to the current goal.

Assume H.

Apply H to the current goal.

Assume H4: y ∉ f Z.

Assume H5: infinite (f Z).

Assume H6: ∀Y ⊆ f Z, equip Y n → C (Y ∪ {y}) ∈ c.

We prove the intermediate claim Ly: y ∈ Z ∧ (y ∉ f Z ∧ ∀Y ⊆ f Z, equip Y n → C (Y ∪ {y}) ∈ c).

Apply andI to the current goal.

An exact proof term for the current goal is Hy.

Apply andI to the current goal.

An exact proof term for the current goal is H4.

An exact proof term for the current goal is H6.

An exact proof term for the current goal is Eps_i_ax (λy ⇒ y ∈ Z ∧ (y ∉ f Z ∧ ∀Y ⊆ f Z, equip Y n → C (Y ∪ {y}) ∈ c)) y Ly.

We prove the intermediate claim Lg1a: ∀Z ⊆ X', infinite Z → g Z ∈ Z ∧ g Z ∉ f Z.

Let Z be given.

Assume HZ1 HZ2.

Apply Lg1 Z HZ1 HZ2 to the current goal.

Assume H3: g Z ∈ Z.

Assume H.

Apply H to the current goal.

Assume H4: g Z ∉ f Z.

Assume _.

Apply andI to the current goal.

An exact proof term for the current goal is H3.

An exact proof term for the current goal is H4.

We prove the intermediate claim Lf': ∃f' : set → set, f' 0 = f X' ∧ ∀m, nat_p m → f' (ordsucc m) = f (f' m).

We use nat_primrec (f X') (λ_ Z ⇒ f Z) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is nat_primrec_0 (f X') (λ_ Z ⇒ f Z).

An exact proof term for the current goal is nat_primrec_S (f X') (λ_ Z ⇒ f Z).

Apply Lf' to the current goal.

Let f' be given.

Assume H.

Apply H to the current goal.

Assume Hf'0 Hf'S.

Apply infiniteRamsey_lem X' f g f' HX' Lf1a Lg1a Hf'0 Hf'S to the current goal.

Assume H.

Apply H to the current goal.

Assume Hf'1: ∀m, nat_p m → f' m ⊆ X' ∧ infinite (f' m).

Assume Hgf'mm'Subq: ∀m m' ∈ ω, m ⊆ m' → f' m' ⊆ f' m.

Assume Hgf'inj: ∀m m' ∈ ω, g (f' m) = g (f' m') → m = m'.

Set H' to be the term {g (f' n)|n ∈ ω}.

We prove the intermediate claim LH'X: H' ⊆ X.

Let u be given.

Assume Hu: u ∈ H'.

Apply ReplE_impred ω (λn ⇒ g (f' n)) u Hu to the current goal.

Let m be given.

Assume Hm: m ∈ ω.

Assume Hue: u = g (f' m).

rewrite the current goal using Hue (from left to right).

We will prove g (f' m) ∈ X.

Apply Hf'1 m (omega_nat_p m Hm) to the current goal.

Assume Hf'mX': f' m ⊆ X'.

Assume Hf'minf: infinite (f' m).

Apply Lg1 (f' m) Hf'mX' Hf'minf to the current goal.

Assume Hgf'm: g (f' m) ∈ f' m.

Assume _.

Apply HX'X to the current goal.

Apply Hf'mX' to the current goal.

An exact proof term for the current goal is Hgf'm.

We prove the intermediate claim LH'inf: infinite H'.

Apply atleastp_omega_infinite to the current goal.

We will prove atleastp ω H'.

We will prove ∃g : set → set, inj ω H' g.

We use (λn : set ⇒ g (f' n)) to witness the existential quantifier.

We will prove (∀m ∈ ω, g (f' m) ∈ H') ∧ (∀m m' ∈ ω, g (f' m) = g (f' m') → m = m').

Apply andI to the current goal.

Let m be given.

Assume Hm: m ∈ ω.

We will prove g (f' m) ∈ {g (f' n)|n ∈ ω}.

An exact proof term for the current goal is ReplI ω (λn ⇒ g (f' n)) m Hm.

An exact proof term for the current goal is Hgf'inj.

We prove the intermediate claim LCSnlem: ∀m, nat_p m → ∀Y ⊆ H', equip Y (ordsucc n) → g (f' m) ∈ Y → (∀k ∈ m, g (f' k) ∉ Y) → C Y ∈ c.

Let m be given.

Assume Hm.

Let Y be given.

Assume HYH': Y ⊆ H'.

Assume HYSn: equip Y (ordsucc n).

Assume Hgf'mY: g (f' m) ∈ Y.

Assume Hgf'kY: ∀k ∈ m, g (f' k) ∉ Y.

Apply Hf'1 m Hm to the current goal.

Assume Hf'mX': f' m ⊆ X'.

Assume Hf'minf: infinite (f' m).

Apply Lg1 (f' m) Hf'mX' Hf'minf to the current goal.

Assume Hgf'mf'm: g (f' m) ∈ f' m.

Assume H.

Apply H to the current goal.

Assume Hgf'mff'm: g (f' m) ∉ f (f' m).

Assume Hgf'mc: ∀Y ⊆ f (f' m), equip Y n → C (Y ∪ {g (f' m)}) ∈ c.

We prove the intermediate claim Lmo: ordinal m.

Apply nat_p_ordinal to the current goal.

An exact proof term for the current goal is Hm.

We will prove C Y ∈ c.

rewrite the current goal using binunion_remove1_eq Y (g (f' m)) Hgf'mY (from left to right).

We will prove C ((Y ∖ {g (f' m)}) ∪ {g (f' m)}) ∈ c.

Apply Hgf'mc to the current goal.

We will prove Y ∖ {g (f' m)} ⊆ f (f' m).

Let u be given.

Assume Hu: u ∈ Y ∖ {g (f' m)}.

We prove the intermediate claim Luf'Sm: u ∈ f' (ordsucc m).

Apply setminusE Y {g (f' m)} u Hu to the current goal.

Assume Hu1: u ∈ Y.

Assume Hu2: u ∉ {g (f' m)}.

Apply ReplE_impred ω (λn ⇒ g (f' n)) u (HYH' u Hu1) to the current goal.

Let k be given.

Assume Hk: k ∈ ω.

Assume Huk: u = g (f' k).

We will prove u ∈ f' (ordsucc m).

We prove the intermediate claim Lko: ordinal k.

Apply nat_p_ordinal to the current goal.

Apply omega_nat_p to the current goal.

An exact proof term for the current goal is Hk.

Apply ordinal_trichotomy_or_impred k m Lko Lmo to the current goal.

Assume Hkm: k ∈ m.

We will prove False.

Apply Hgf'kY k Hkm to the current goal.

We will prove g (f' k) ∈ Y.

rewrite the current goal using Huk (from right to left).

An exact proof term for the current goal is Hu1.

Assume Hkm: k = m.

We will prove False.

Apply Hu2 to the current goal.

rewrite the current goal using Huk (from left to right).

We will prove g (f' k) ∈ {g (f' m)}.

rewrite the current goal using Hkm (from left to right).

Apply SingI to the current goal.

Assume Hmk: m ∈ k.

We will prove u ∈ f' (ordsucc m).

Apply Hgf'mm'Subq (ordsucc m) (omega_ordsucc m (nat_p_omega m Hm)) k Hk to the current goal.

We will prove ordsucc m ⊆ k.

An exact proof term for the current goal is ordinal_ordsucc_In_Subq k Lko m Hmk.

We will prove u ∈ f' k.

rewrite the current goal using Huk (from left to right).

We will prove g (f' k) ∈ f' k.

Apply Hf'1 k (omega_nat_p k Hk) to the current goal.

Assume Hf'kX': f' k ⊆ X'.

Assume Hf'kinf: infinite (f' k).

Apply Lg1 (f' k) Hf'kX' Hf'kinf to the current goal.

Assume Hgf'kf'k: g (f' k) ∈ f' k.

Assume _.

An exact proof term for the current goal is Hgf'kf'k.

We will prove u ∈ f (f' m).

An exact proof term for the current goal is Hf'S m Hm (λw _ ⇒ u ∈ w) Luf'Sm.

We will prove equip (Y ∖ {g (f' m)}) n.

Apply equip_ordsucc_remove1 to the current goal.

An exact proof term for the current goal is Hgf'mY.

We will prove equip Y (ordsucc n).

An exact proof term for the current goal is HYSn.

We prove the intermediate claim LCSn: ∀Y ⊆ H', equip Y (ordsucc n) → C Y ∈ c.

Let Y be given.

Assume HYH': Y ⊆ H'.

Assume HYSn: equip Y (ordsucc n).

We will prove C Y ∈ c.

Set p to be the term λm ⇒ m ∈ ω ∧ g (f' m) ∈ Y of type set → prop.

We prove the intermediate claim Lpne: ∃m, ordinal m ∧ p m.

Apply equip_sym Y (ordsucc n) HYSn to the current goal.

Let h be given.

Assume Hh: bij (ordsucc n) Y h.

Apply Hh to the current goal.

Assume H _.

Apply H to the current goal.

Assume Hh1: ∀i ∈ ordsucc n, h i ∈ Y.

Assume _.

We prove the intermediate claim LhnY: h n ∈ Y.

Apply Hh1 to the current goal.

Apply ordsuccI2 to the current goal.

Apply ReplE_impred ω (λn ⇒ g (f' n)) (h n) (HYH' (h n) LhnY) to the current goal.

Let m be given.

Assume Hm: m ∈ ω.

Assume Hhnm: h n = g (f' m).

We use m to witness the existential quantifier.

Apply andI to the current goal.

We will prove ordinal m.

Apply nat_p_ordinal to the current goal.

Apply omega_nat_p to the current goal.

An exact proof term for the current goal is Hm.

We will prove m ∈ ω ∧ g (f' m) ∈ Y.

Apply andI to the current goal.

An exact proof term for the current goal is Hm.

rewrite the current goal using Hhnm (from right to left).

An exact proof term for the current goal is LhnY.

Apply least_ordinal_ex p Lpne to the current goal.

Let m be given.

Assume H.

Apply H to the current goal.

Assume H.

Apply H to the current goal.

Assume Hmo: ordinal m.

Assume Hpm: m ∈ ω ∧ g (f' m) ∈ Y.

Assume Hpk: ∀k ∈ m, ¬ (k ∈ ω ∧ g (f' k) ∈ Y).

Apply Hpm to the current goal.

Assume Hm: m ∈ ω.

Assume Hgf'm: g (f' m) ∈ Y.

We will prove C Y ∈ c.

Apply LCSnlem m (omega_nat_p m Hm) Y HYH' HYSn Hgf'm to the current goal.

Let k be given.

Assume Hk: k ∈ m.

We will prove g (f' k) ∉ Y.

Assume Hgf'k: g (f' k) ∈ Y.

Apply Hpk k Hk to the current goal.

Apply andI to the current goal.

We will prove k ∈ ω.

Apply nat_p_omega to the current goal.

An exact proof term for the current goal is nat_p_trans m (omega_nat_p m Hm) k Hk.

We will prove g (f' k) ∈ Y.

An exact proof term for the current goal is Hgf'k.

Apply IHc (ordsucc n) (nat_ordsucc n Hn) H' LH'inf C LCSn to the current goal.

Let H'' be given.

Assume H.

Apply H to the current goal.

Assume HH''H': H'' ⊆ H'.

Assume H.

Apply H to the current goal.

Let i be given.

Assume H.

Apply H to the current goal.

Assume Hi: i ∈ c.

Assume H.

Apply H to the current goal.

Assume HH''inf: infinite H''.

Assume HH''hom: ∀Y ⊆ H'', equip Y (ordsucc n) → C Y = i.

Apply H2 to the current goal.

We use H'' to witness the existential quantifier.

Apply andI to the current goal.

We will prove H'' ⊆ X.

An exact proof term for the current goal is Subq_tra H'' H' X HH''H' LH'X.

We use i to witness the existential quantifier.

Apply andI to the current goal.

We will prove i ∈ ordsucc c.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is Hi.

Apply andI to the current goal.

We will prove infinite H''.

An exact proof term for the current goal is HH''inf.

We will prove ∀Y ⊆ H'', equip Y (ordsucc n) → C Y = i.

An exact proof term for the current goal is HH''hom.

Set f to be the term λX' ⇒ Eps_i (λX'' ⇒ X'' ⊆ X' ∧ ∃x ∈ X', x ∉ X'' ∧ infinite X'' ∧ ∀Y ⊆ X'', equip Y n → C (Y ∪ {x}) = c) of type set → set.

We prove the intermediate claim Lf1: ∀X' ⊆ X, infinite X' → f X' ⊆ X' ∧ ∃x ∈ X', x ∉ f X' ∧ infinite (f X') ∧ ∀Y ⊆ f X', equip Y n → C (Y ∪ {x}) = c.

Let X' be given.

Assume HX'X HX'inf.

An exact proof term for the current goal is Eps_i_ex (λX'' ⇒ X'' ⊆ X' ∧ ∃x ∈ X', x ∉ X'' ∧ infinite X'' ∧ ∀Y ⊆ X'', equip Y n → C (Y ∪ {x}) = c) (L1 X' HX'X HX'inf).

We prove the intermediate claim Lf1a: ∀Z ⊆ X, infinite Z → f Z ⊆ Z ∧ infinite (f Z).

Let Z be given.

Assume HZ1 HZ2.

Apply Lf1 Z HZ1 HZ2 to the current goal.

Assume H3: f Z ⊆ Z.

Assume H.

Apply H to the current goal.

Let y be given.

Assume H.

Apply H to the current goal.

Assume Hy: y ∈ Z.

Assume H.

Apply H to the current goal.

Assume H4: y ∉ f Z ∧ infinite (f Z).

Assume _.

Apply H4 to the current goal.

Assume _.

Assume H5: infinite (f Z).

Apply andI to the current goal.

An exact proof term for the current goal is H3.

An exact proof term for the current goal is H5.

Set g to be the term λX' ⇒ Eps_i (λx ⇒ x ∈ X' ∧ (x ∉ f X' ∧ ∀Y ⊆ f X', equip Y n → C (Y ∪ {x}) = c)) of type set → set.

We prove the intermediate claim Lg1: ∀X' ⊆ X, infinite X' → g X' ∈ X' ∧ (g X' ∉ f X' ∧ ∀Y ⊆ f X', equip Y n → C (Y ∪ {g X'}) = c).

Let X' be given.

Assume HX'X HX'inf.

Apply Lf1 X' HX'X HX'inf to the current goal.

Assume HfX'X': f X' ⊆ X'.

Assume H.

Apply H to the current goal.

Let x be given.

Assume H.

Apply H to the current goal.

Assume Hx: x ∈ X'.

Assume H.

Apply H to the current goal.

Assume H.

Apply H to the current goal.

Assume HxfX': x ∉ f X'.

Assume HfX'inf: infinite (f X').

Assume HfX'hom: ∀Y ⊆ f X', equip Y n → C (Y ∪ {x}) = c.

We prove the intermediate claim Lg1': x ∈ X' ∧ (x ∉ f X' ∧ ∀Y ⊆ f X', equip Y n → C (Y ∪ {x}) = c).

Apply andI to the current goal.

An exact proof term for the current goal is Hx.

Apply andI to the current goal.

An exact proof term for the current goal is HxfX'.

An exact proof term for the current goal is HfX'hom.

An exact proof term for the current goal is Eps_i_ax (λx ⇒ x ∈ X' ∧ (x ∉ f X' ∧ ∀Y ⊆ f X', equip Y n → C (Y ∪ {x}) = c)) x Lg1'.

We prove the intermediate claim Lg1a: ∀Z ⊆ X, infinite Z → g Z ∈ Z ∧ g Z ∉ f Z.

Let Z be given.

Assume HZ1 HZ2.

Apply Lg1 Z HZ1 HZ2 to the current goal.

Assume H3: g Z ∈ Z.

Assume H.

Apply H to the current goal.

Assume H4: g Z ∉ f Z.

Assume _.

Apply andI to the current goal.

An exact proof term for the current goal is H3.

An exact proof term for the current goal is H4.

We prove the intermediate claim Lf': ∃f' : set → set, f' 0 = f X ∧ ∀m, nat_p m → f' (ordsucc m) = f (f' m).

We use nat_primrec (f X) (λ_ Z ⇒ f Z) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is nat_primrec_0 (f X) (λ_ Z ⇒ f Z).

An exact proof term for the current goal is nat_primrec_S (f X) (λ_ Z ⇒ f Z).

Apply Lf' to the current goal.

Let f' be given.

Assume H.

Apply H to the current goal.

Assume Hf'0 Hf'S.

Apply infiniteRamsey_lem X f g f' HX Lf1a Lg1a Hf'0 Hf'S to the current goal.

Assume H.

Apply H to the current goal.

Assume Hf'1: ∀m, nat_p m → f' m ⊆ X ∧ infinite (f' m).

Assume Hgf'mm'Subq: ∀m m' ∈ ω, m ⊆ m' → f' m' ⊆ f' m.

Assume Hgf'inj: ∀m m' ∈ ω, g (f' m) = g (f' m') → m = m'.

Set H' to be the term {g (f' n)|n ∈ ω}.

We prove the intermediate claim Lf'1: ∀m, nat_p m → f' m ⊆ X ∧ infinite (f' m).

Apply nat_ind to the current goal.

rewrite the current goal using Hf'0 (from left to right).

We will prove f X ⊆ X ∧ infinite (f X).

Apply Lf1 X (λu H ⇒ H) HX to the current goal.

Assume H3: f X ⊆ X.

Assume H.

Apply H to the current goal.

Let y be given.

Assume H.

Apply H to the current goal.

Assume _ H.

Apply H to the current goal.

Assume H.

Apply H to the current goal.

Assume _.

Assume H4: infinite (f X).

Assume _.

We will prove f X ⊆ X ∧ infinite (f X).

Apply andI to the current goal.

An exact proof term for the current goal is H3.

An exact proof term for the current goal is H4.

Let m be given.

Assume Hm.

Assume IHm.

Apply IHm to the current goal.

Assume IHm1: f' m ⊆ X.

Assume IHm2: infinite (f' m).

We will prove f' (ordsucc m) ⊆ X ∧ infinite (f' (ordsucc m)).

rewrite the current goal using Hf'S m Hm (from left to right).

We will prove f (f' m) ⊆ X ∧ infinite (f (f' m)).

Apply Lf1 (f' m) IHm1 IHm2 to the current goal.

Assume H3: f (f' m) ⊆ f' m.

Assume H.

Apply H to the current goal.

Let y be given.

Assume H.

Apply H to the current goal.

Assume _ H.

Apply H to the current goal.

Assume H.

Apply H to the current goal.

Assume _.

Assume H4: infinite (f (f' m)).

Assume _.

Apply andI to the current goal.

Apply Subq_tra (f (f' m)) (f' m) X H3 to the current goal.

An exact proof term for the current goal is IHm1.

An exact proof term for the current goal is H4.

We prove the intermediate claim Lgf'mm'addSubq: ∀m ∈ ω, ∀m', nat_p m' → f' (m + m') ⊆ f' m.

Let m be given.

Assume Hm.

Apply nat_ind to the current goal.

We will prove f' (m + 0) ⊆ f' m.

rewrite the current goal using add_nat_0R m (from left to right).

An exact proof term for the current goal is Subq_ref (f' m).

Let m' be given.

Assume Hm'.

Assume IHm': f' (m + m') ⊆ f' m.

We will prove f' (m + ordsucc m') ⊆ f' m.

rewrite the current goal using add_nat_SR m m' Hm' (from left to right).

We will prove f' (ordsucc (m + m')) ⊆ f' m.

rewrite the current goal using Hf'S (m + m') (add_nat_p m (omega_nat_p m Hm) m' Hm') (from left to right).

We will prove f (f' (m + m')) ⊆ f' m.

Apply Subq_tra (f (f' (m + m'))) (f' (m + m')) (f' m) to the current goal.

Apply Lf'1 (m + m') (add_nat_p m (omega_nat_p m Hm) m' Hm') to the current goal.

Assume Hfmm'X: f' (m + m') ⊆ X.

Assume Hfmm'inf: infinite (f' (m + m')).

Apply Lf1 (f' (m + m')) Hfmm'X Hfmm'inf to the current goal.

Assume H3: f (f' (m + m')) ⊆ f' (m + m').

Assume _.

An exact proof term for the current goal is H3.

An exact proof term for the current goal is IHm'.

We prove the intermediate claim Lgf'mm'Subq: ∀m m' ∈ ω, m ⊆ m' → f' m' ⊆ f' m.

Let m be given.

Assume Hm: m ∈ ω.

Let m' be given.

Assume Hm': m' ∈ ω.

Assume Hmm': m ⊆ m'.

Apply nat_Subq_add_ex m (omega_nat_p m Hm) m' (omega_nat_p m' Hm') Hmm' to the current goal.

Let k be given.

Assume H.

Apply H to the current goal.

Assume Hk: nat_p k.

Assume Hm'km: m' = k + m.

We will prove f' m' ⊆ f' m.

rewrite the current goal using Hm'km (from left to right).

We will prove f' (k + m) ⊆ f' m.

rewrite the current goal using add_nat_com k Hk m (omega_nat_p m Hm) (from left to right).

We will prove f' (m + k) ⊆ f' m.

An exact proof term for the current goal is Lgf'mm'addSubq m Hm k Hk.

We prove the intermediate claim Lgf'injlem: ∀m ∈ ω, ∀m' ∈ m, g (f' m') ≠ g (f' m).

Let m be given.

Assume Hm: m ∈ ω.

Let m' be given.

Assume Hm': m' ∈ m.

Assume H3: g (f' m') = g (f' m).

We prove the intermediate claim LmN: nat_p m.

Apply omega_nat_p to the current goal.

An exact proof term for the current goal is Hm.

We prove the intermediate claim Lmo: ordinal m.

Apply nat_p_ordinal to the current goal.

An exact proof term for the current goal is LmN.

We prove the intermediate claim Lm'N: nat_p m'.

An exact proof term for the current goal is nat_p_trans m (omega_nat_p m Hm) m' Hm'.

We prove the intermediate claim Lf'mff'm': f' m ⊆ f (f' m').

Apply Hf'S m' Lm'N (λu _ ⇒ f' m ⊆ u) to the current goal.

We will prove f' m ⊆ f' (ordsucc m').

Apply Lgf'mm'Subq (ordsucc m') (omega_ordsucc m' (nat_p_omega m' Lm'N)) m Hm to the current goal.

We will prove ordsucc m' ⊆ m.

An exact proof term for the current goal is ordinal_ordsucc_In_Subq m Lmo m' Hm'.

Apply Lf'1 m (omega_nat_p m Hm) to the current goal.

Assume H4: f' m ⊆ X.

Assume H5: infinite (f' m).

Apply Lg1 (f' m) H4 H5 to the current goal.

Assume H6: g (f' m) ∈ f' m.

Assume _.

Apply Lf'1 m' Lm'N to the current goal.

Assume H7: f' m' ⊆ X.

Assume H8: infinite (f' m').

Apply Lg1 (f' m') H7 H8 to the current goal.

Assume _ H.

Apply H to the current goal.

Assume H9: g (f' m') ∉ f (f' m').

Assume _.

Apply H9 to the current goal.

We will prove g (f' m') ∈ f (f' m').

rewrite the current goal using H3 (from left to right).

We will prove g (f' m) ∈ f (f' m').

An exact proof term for the current goal is Lf'mff'm' (g (f' m)) H6.

We prove the intermediate claim Lgf'inj: ∀m m' ∈ ω, g (f' m) = g (f' m') → m = m'.

Let m be given.

Assume Hm: m ∈ ω.

Let m' be given.

Assume Hm': m' ∈ ω.

Assume Hgf'mm': g (f' m) = g (f' m').

Apply ordinal_trichotomy_or_impred m m' (nat_p_ordinal m (omega_nat_p m Hm)) (nat_p_ordinal m' (omega_nat_p m' Hm')) to the current goal.

Assume Hmm': m ∈ m'.

We will prove False.

Apply Lgf'injlem m' Hm' m Hmm' to the current goal.

We will prove g (f' m) = g (f' m').

An exact proof term for the current goal is Hgf'mm'.

Assume Hmm': m = m'.

An exact proof term for the current goal is Hmm'.

Assume Hm'm: m' ∈ m.

We will prove False.

Apply Lgf'injlem m Hm m' Hm'm to the current goal.

We will prove g (f' m') = g (f' m).

Use symmetry.

An exact proof term for the current goal is Hgf'mm'.

We prove the intermediate claim LH'X: H' ⊆ X.

Let u be given.

Assume Hu: u ∈ H'.

Apply ReplE_impred ω (λn ⇒ g (f' n)) u Hu to the current goal.

Let m be given.

Assume Hm: m ∈ ω.

Assume Hue: u = g (f' m).

rewrite the current goal using Hue (from left to right).

We will prove g (f' m) ∈ X.

Apply Lf'1 m (omega_nat_p m Hm) to the current goal.

Assume Hf'mX: f' m ⊆ X.

Assume Hf'minf: infinite (f' m).

Apply Lg1 (f' m) Hf'mX Hf'minf to the current goal.

Assume Hgf'm: g (f' m) ∈ f' m.

Assume _.

Apply Hf'mX to the current goal.

An exact proof term for the current goal is Hgf'm.

We prove the intermediate claim LH'inf: infinite H'.

Apply atleastp_omega_infinite to the current goal.

We will prove atleastp ω H'.

We will prove ∃g : set → set, inj ω H' g.

We use (λn : set ⇒ g (f' n)) to witness the existential quantifier.

We will prove (∀m ∈ ω, g (f' m) ∈ H') ∧ (∀m m' ∈ ω, g (f' m) = g (f' m') → m = m').

Apply andI to the current goal.

Let m be given.

Assume Hm: m ∈ ω.

We will prove g (f' m) ∈ {g (f' n)|n ∈ ω}.

An exact proof term for the current goal is ReplI ω (λn ⇒ g (f' n)) m Hm.

An exact proof term for the current goal is Lgf'inj.

We prove the intermediate claim LCSnlem: ∀m, nat_p m → ∀Y ⊆ H', equip Y (ordsucc n) → g (f' m) ∈ Y → (∀k ∈ m, g (f' k) ∉ Y) → C Y = c.

Let m be given.

Assume Hm.

Let Y be given.

Assume HYH': Y ⊆ H'.

Assume HYSn: equip Y (ordsucc n).

Assume Hgf'mY: g (f' m) ∈ Y.

Assume Hgf'kY: ∀k ∈ m, g (f' k) ∉ Y.

Apply Lf'1 m Hm to the current goal.

Assume Hf'mX: f' m ⊆ X.

Assume Hf'minf: infinite (f' m).

Apply Lg1 (f' m) Hf'mX Hf'minf to the current goal.

Assume Hgf'mf'm: g (f' m) ∈ f' m.

Assume H.

Apply H to the current goal.

Assume Hgf'mff'm: g (f' m) ∉ f (f' m).

Assume Hgf'mc: ∀Y ⊆ f (f' m), equip Y n → C (Y ∪ {g (f' m)}) = c.

We prove the intermediate claim Lmo: ordinal m.

Apply nat_p_ordinal to the current goal.

An exact proof term for the current goal is Hm.

We will prove C Y = c.

rewrite the current goal using binunion_remove1_eq Y (g (f' m)) Hgf'mY (from left to right).

We will prove C ((Y ∖ {g (f' m)}) ∪ {g (f' m)}) = c.

Apply Hgf'mc to the current goal.

We will prove Y ∖ {g (f' m)} ⊆ f (f' m).

Let u be given.

Assume Hu: u ∈ Y ∖ {g (f' m)}.

We prove the intermediate claim Luf'Sm: u ∈ f' (ordsucc m).

Apply setminusE Y {g (f' m)} u Hu to the current goal.

Assume Hu1: u ∈ Y.

Assume Hu2: u ∉ {g (f' m)}.

Apply ReplE_impred ω (λn ⇒ g (f' n)) u (HYH' u Hu1) to the current goal.

Let k be given.

Assume Hk: k ∈ ω.

Assume Huk: u = g (f' k).

We will prove u ∈ f' (ordsucc m).

We prove the intermediate claim Lko: ordinal k.

Apply nat_p_ordinal to the current goal.

Apply omega_nat_p to the current goal.

An exact proof term for the current goal is Hk.

Apply ordinal_trichotomy_or_impred k m Lko Lmo to the current goal.

Assume Hkm: k ∈ m.

We will prove False.

Apply Hgf'kY k Hkm to the current goal.

We will prove g (f' k) ∈ Y.

rewrite the current goal using Huk (from right to left).

An exact proof term for the current goal is Hu1.

Assume Hkm: k = m.

We will prove False.

Apply Hu2 to the current goal.

rewrite the current goal using Huk (from left to right).

We will prove g (f' k) ∈ {g (f' m)}.

rewrite the current goal using Hkm (from left to right).

Apply SingI to the current goal.

Assume Hmk: m ∈ k.

We will prove u ∈ f' (ordsucc m).

Apply Lgf'mm'Subq (ordsucc m) (omega_ordsucc m (nat_p_omega m Hm)) k Hk to the current goal.

We will prove ordsucc m ⊆ k.

An exact proof term for the current goal is ordinal_ordsucc_In_Subq k Lko m Hmk.

We will prove u ∈ f' k.

rewrite the current goal using Huk (from left to right).

We will prove g (f' k) ∈ f' k.

Apply Lf'1 k (omega_nat_p k Hk) to the current goal.

Assume Hf'kX: f' k ⊆ X.

Assume Hf'kinf: infinite (f' k).

Apply Lg1 (f' k) Hf'kX Hf'kinf to the current goal.

Assume Hgf'kf'k: g (f' k) ∈ f' k.

Assume _.

An exact proof term for the current goal is Hgf'kf'k.

We will prove u ∈ f (f' m).

An exact proof term for the current goal is Hf'S m Hm (λw _ ⇒ u ∈ w) Luf'Sm.

We will prove equip (Y ∖ {g (f' m)}) n.

Apply equip_ordsucc_remove1 to the current goal.

An exact proof term for the current goal is Hgf'mY.

We will prove equip Y (ordsucc n).

An exact proof term for the current goal is HYSn.

We prove the intermediate claim LCSn: ∀Y ⊆ H', equip Y (ordsucc n) → C Y = c.

Let Y be given.

Assume HYH': Y ⊆ H'.

Assume HYSn: equip Y (ordsucc n).

We will prove C Y = c.

Set p to be the term λm ⇒ m ∈ ω ∧ g (f' m) ∈ Y of type set → prop.

We prove the intermediate claim Lpne: ∃m, ordinal m ∧ p m.

Apply equip_sym Y (ordsucc n) HYSn to the current goal.

Let h be given.

Assume Hh: bij (ordsucc n) Y h.

Apply Hh to the current goal.

Assume H _.

Apply H to the current goal.

Assume Hh1: ∀i ∈ ordsucc n, h i ∈ Y.

Assume _.

We prove the intermediate claim LhnY: h n ∈ Y.

Apply Hh1 to the current goal.

Apply ordsuccI2 to the current goal.

Apply ReplE_impred ω (λn ⇒ g (f' n)) (h n) (HYH' (h n) LhnY) to the current goal.

Let m be given.

Assume Hm: m ∈ ω.

Assume Hhnm: h n = g (f' m).

We use m to witness the existential quantifier.

Apply andI to the current goal.

We will prove ordinal m.

Apply nat_p_ordinal to the current goal.

Apply omega_nat_p to the current goal.

An exact proof term for the current goal is Hm.

We will prove m ∈ ω ∧ g (f' m) ∈ Y.

Apply andI to the current goal.

An exact proof term for the current goal is Hm.

rewrite the current goal using Hhnm (from right to left).

An exact proof term for the current goal is LhnY.

Apply least_ordinal_ex p Lpne to the current goal.

Let m be given.

Assume H.

Apply H to the current goal.

Assume H.

Apply H to the current goal.

Assume Hmo: ordinal m.

Assume Hpm: m ∈ ω ∧ g (f' m) ∈ Y.

Assume Hpk: ∀k ∈ m, ¬ (k ∈ ω ∧ g (f' k) ∈ Y).

Apply Hpm to the current goal.

Assume Hm: m ∈ ω.

Assume Hgf'm: g (f' m) ∈ Y.

We will prove C Y = c.

Apply LCSnlem m (omega_nat_p m Hm) Y HYH' HYSn Hgf'm to the current goal.

Let k be given.

Assume Hk: k ∈ m.

We will prove g (f' k) ∉ Y.

Assume Hgf'k: g (f' k) ∈ Y.

Apply Hpk k Hk to the current goal.

Apply andI to the current goal.

We will prove k ∈ ω.

Apply nat_p_omega to the current goal.

An exact proof term for the current goal is nat_p_trans m (omega_nat_p m Hm) k Hk.

We will prove g (f' k) ∈ Y.

An exact proof term for the current goal is Hgf'k.

Apply H2 to the current goal.

We use H' to witness the existential quantifier.

Apply andI to the current goal.

We will prove H' ⊆ X.

An exact proof term for the current goal is LH'X.

We use c to witness the existential quantifier.

Apply andI to the current goal.

Apply ordsuccI2 to the current goal.

Apply andI to the current goal.

We will prove infinite H'.

An exact proof term for the current goal is LH'inf.

An exact proof term for the current goal is LCSn.