Let S1, S2 and n be given.
Assume Heq: equip S1 S2.
Assume Hcard: cardinality_at_most S2 n.
We prove the intermediate claim HnOrd: ordinal n.
An exact proof term for the current goal is (andEL (ordinal n) (∃k : set, ordinal k ∧ k ⊆ n ∧ equip S2 k) Hcard).
We prove the intermediate claim Hexk: ∃k : set, ordinal k ∧ k ⊆ n ∧ equip S2 k.
An exact proof term for the current goal is (andER (ordinal n) (∃k : set, ordinal k ∧ k ⊆ n ∧ equip S2 k) Hcard).
We will prove cardinality_at_most S1 n.
We prove the intermediate claim Hcore: ordinal n ∧ ∃k : set, ordinal k ∧ k ⊆ n ∧ equip S1 k.
Apply andI to the current goal.
An exact proof term for the current goal is HnOrd.
Apply Hexk to the current goal.
Let k be given.
Assume Hkpack: ordinal k ∧ k ⊆ n ∧ equip S2 k.
We use k to witness the existential quantifier.
We will prove (ordinal k ∧ k ⊆ n) ∧ equip S1 k.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (ordinal k ∧ k ⊆ n) (equip S2 k) Hkpack).
We prove the intermediate claim HeqS2k: equip S2 k.
An exact proof term for the current goal is (andER (ordinal k ∧ k ⊆ n) (equip S2 k) Hkpack).
An exact proof term for the current goal is (equip_tra S1 S2 k Heq HeqS2k).
An exact proof term for the current goal is Hcore.
∎