Let n and S be given.
Assume HnNat: nat_p n.
Assume HSsub: S ⊆ n.
Set p to be the term (λt : set ⇒ ∀S0 : set, S0 ⊆ t → ∃m : set, nat_p m ∧ (m ⊆ t ∧ equip S0 m)).
We prove the intermediate claim Hp0: p 0.
Let S0 be given.
Assume HS0: S0 ⊆ 0.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is nat_0.
Apply andI to the current goal.
An exact proof term for the current goal is (Subq_ref 0).
We prove the intermediate claim HS0eq: S0 = 0.
Apply set_ext to the current goal.
An exact proof term for the current goal is HS0.
Let x be given.
Assume Hx0: x ∈ 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((EmptyE x) Hx0).
rewrite the current goal using HS0eq (from left to right).
An exact proof term for the current goal is (equip_ref 0).
We prove the intermediate claim HpS: ∀t : set, nat_p t → p t → p (ordsucc t).
Let t be given.
Assume HtNat: nat_p t.
Assume Hpt: p t.
We will prove p (ordsucc t).
Let S0 be given.
Assume HS0sub: S0 ⊆ ordsucc t.
Apply (xm (t ∈ S0)) to the current goal.
Assume HtInS0: t ∈ S0.
Set S1 to be the term S0 ∖ {t}.
We prove the intermediate claim HS1subt: S1 ⊆ t.
Let x be given.
Assume HxS1: x ∈ S1.
We prove the intermediate claim HxS0: x ∈ S0.
An exact proof term for the current goal is (setminusE1 S0 {t} x HxS1).
We prove the intermediate claim HxSucc: x ∈ ordsucc t.
An exact proof term for the current goal is (HS0sub x HxS0).
Apply (ordsuccE t x HxSucc) to the current goal.
Assume Hxt: x ∈ t.
An exact proof term for the current goal is Hxt.
Assume Hxeq: x = t.
Apply FalseE to the current goal.
We prove the intermediate claim Hxnot: x ∉ {t}.
An exact proof term for the current goal is (setminusE2 S0 {t} x HxS1).
We prove the intermediate claim HxIn: x ∈ {t}.
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is (SingI t).
An exact proof term for the current goal is (Hxnot HxIn).
We prove the intermediate claim Hexm: ∃m : set, nat_p m ∧ (m ⊆ t ∧ equip S1 m).
An exact proof term for the current goal is (Hpt S1 HS1subt).
Apply Hexm to the current goal.
Let m be given.
Assume Hmpack: nat_p m ∧ (m ⊆ t ∧ equip S1 m).
We prove the intermediate claim HmNat: nat_p m.
An exact proof term for the current goal is (andEL (nat_p m) (m ⊆ t ∧ equip S1 m) Hmpack).
We prove the intermediate claim HmTail: m ⊆ t ∧ equip S1 m.
An exact proof term for the current goal is (andER (nat_p m) (m ⊆ t ∧ equip S1 m) Hmpack).
We prove the intermediate claim HmSubt: m ⊆ t.
An exact proof term for the current goal is (andEL (m ⊆ t) (equip S1 m) HmTail).
We prove the intermediate claim HeqS1m: equip S1 m.
An exact proof term for the current goal is (andER (m ⊆ t) (equip S1 m) HmTail).
We prove the intermediate claim HtNotS1: t ∉ S1.
Assume HtS1: t ∈ S1.
We prove the intermediate claim HtNot: t ∉ {t}.
An exact proof term for the current goal is (setminusE2 S0 {t} t HtS1).
An exact proof term for the current goal is (HtNot (SingI t)).
We prove the intermediate claim HeqmS1: equip m S1.
An exact proof term for the current goal is (equip_sym S1 m HeqS1m).
We prove the intermediate claim HeqSucc: equip (ordsucc m) (S1 ∪ {t}).
An exact proof term for the current goal is (equip_adjoin_ordsucc m S1 t HtNotS1 HeqmS1).
We prove the intermediate claim HS0eq: S0 = S1 ∪ {t}.
Apply set_ext to the current goal.
Let x be given.
Assume HxS0: x ∈ S0.
Apply (xm (x = t)) to the current goal.
Assume Hxeq: x = t.
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is (binunionI2 S1 {t} t (SingI t)).
Assume Hxneq: ¬ (x = t).
We prove the intermediate claim HxnotSing: x ∉ {t}.
Assume HxSing: x ∈ {t}.
An exact proof term for the current goal is (Hxneq (SingE t x HxSing)).
We prove the intermediate claim HxS1: x ∈ S1.
An exact proof term for the current goal is (setminusI S0 {t} x HxS0 HxnotSing).
An exact proof term for the current goal is (binunionI1 S1 {t} x HxS1).
Let x be given.
Assume HxUnion: x ∈ S1 ∪ {t}.
Apply (binunionE S1 {t} x HxUnion) to the current goal.
Assume HxS1: x ∈ S1.
An exact proof term for the current goal is (setminusE1 S0 {t} x HxS1).
Assume HxSing: x ∈ {t}.
We prove the intermediate claim Hxeq: x = t.
An exact proof term for the current goal is (SingE t x HxSing).
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is HtInS0.
Set m1 to be the term ordsucc m.
We use m1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (nat_ordsucc m HmNat).
Apply andI to the current goal.
Let z be given.
Assume Hz: z ∈ ordsucc m.
We prove the intermediate claim Hzcase: z ∈ m ∨ z = m.
An exact proof term for the current goal is (ordsuccE m z Hz).
Apply Hzcase to the current goal.
Assume Hzm: z ∈ m.
We prove the intermediate claim Hzt: z ∈ t.
An exact proof term for the current goal is (HmSubt z Hzm).
An exact proof term for the current goal is (ordsuccI1 t z Hzt).
Assume Hzeq: z = m.
rewrite the current goal using Hzeq (from left to right).
Apply (ordinal_trichotomy_or_impred m t (nat_p_ordinal m HmNat) (nat_p_ordinal t HtNat) (m ∈ ordsucc t)) to the current goal.
Assume HmInT: m ∈ t.
An exact proof term for the current goal is (ordsuccI1 t m HmInT).
Assume HmEqT: m = t.
rewrite the current goal using HmEqT (from left to right).
An exact proof term for the current goal is (ordsuccI2 t).
Assume HtInm: t ∈ m.
Apply FalseE to the current goal.
We prove the intermediate claim HtInT: t ∈ t.
An exact proof term for the current goal is (HmSubt t HtInm).
An exact proof term for the current goal is ((In_irref t) HtInT).
rewrite the current goal using HS0eq (from left to right).
An exact proof term for the current goal is (equip_sym (ordsucc m) (S1 ∪ {t}) HeqSucc).
Assume HtNotInS0: t ∉ S0.
We prove the intermediate claim HS0subt: S0 ⊆ t.
Let x be given.
Assume HxS0: x ∈ S0.
We prove the intermediate claim HxSucc: x ∈ ordsucc t.
An exact proof term for the current goal is (HS0sub x HxS0).
Apply (ordsuccE t x HxSucc) to the current goal.
Assume Hxt: x ∈ t.
An exact proof term for the current goal is Hxt.
Assume Hxeq: x = t.
Apply FalseE to the current goal.
We prove the intermediate claim HtS0: t ∈ S0.
rewrite the current goal using Hxeq (from right to left).
An exact proof term for the current goal is HxS0.
An exact proof term for the current goal is (HtNotInS0 HtS0).
We prove the intermediate claim Hexm: ∃m : set, nat_p m ∧ (m ⊆ t ∧ equip S0 m).
An exact proof term for the current goal is (Hpt S0 HS0subt).
Apply Hexm to the current goal.
Let m be given.
Assume Hm: nat_p m ∧ (m ⊆ t ∧ equip S0 m).
We use m to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (nat_p m) (m ⊆ t ∧ equip S0 m) Hm).
Apply andI to the current goal.
An exact proof term for the current goal is (Subq_tra m t (ordsucc t) (andEL (m ⊆ t) (equip S0 m) (andER (nat_p m) (m ⊆ t ∧ equip S0 m) Hm)) (ordsuccI1 t)).
An exact proof term for the current goal is (andER (m ⊆ t) (equip S0 m) (andER (nat_p m) (m ⊆ t ∧ equip S0 m) Hm)).
We prove the intermediate claim HpN: p n.
An exact proof term for the current goal is (nat_ind p Hp0 HpS n HnNat).
An exact proof term for the current goal is (HpN S HSsub).
∎