Let F be given.
Assume HFfin: finite F.
Apply HFfin to the current goal.
Let n be given.
Assume Hnpack: n ∈ ω ∧ equip F n.
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (andEL (n ∈ ω) (equip F n) Hnpack).
We prove the intermediate claim Hequip: equip F n.
An exact proof term for the current goal is (andER (n ∈ ω) (equip F n) Hnpack).
Apply Hequip to the current goal.
Let f be given.
Assume Hbij: bij F n f.
Apply Hbij to the current goal.
Assume Hcore Hsurj.
Apply Hcore to the current goal.
Assume Hmap Hinj.
Set e to be the term graph n (λy : set ⇒ inv F f y).
We prove the intermediate claim Hrinv: ∀y : set, y ∈ n → inv F f y ∈ F ∧ f (inv F f y) = y.
Let y be given.
Assume HyN: y ∈ n.
An exact proof term for the current goal is (surj_rinv F n f Hsurj y HyN).
We prove the intermediate claim He_map: ∀y : set, y ∈ n → inv F f y ∈ F.
Let y be given.
Assume HyN: y ∈ n.
An exact proof term for the current goal is (andEL (inv F f y ∈ F) (f (inv F f y) = y) (Hrinv y HyN)).
We prove the intermediate claim He_fun: function_on e n F.
We prove the intermediate claim Htot: total_function_on e n F.
Apply (total_function_on_graph n F (λy : set ⇒ inv F f y)) to the current goal.
Let y be given.
Assume HyN: y ∈ n.
An exact proof term for the current goal is (He_map y HyN).
An exact proof term for the current goal is (total_function_on_function_on e n F Htot).
We use n to witness the existential quantifier.
We use e to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HnO.
We will prove bijection n F e.
We will prove function_on e n F ∧ (∀x : set, x ∈ F → ∃y : set, y ∈ n ∧ apply_fun e y = x ∧ (∀y' : set, y' ∈ n → apply_fun e y' = x → y' = y)).
Apply andI to the current goal.
An exact proof term for the current goal is He_fun.
Let x be given.
Assume HxF: x ∈ F.
Set y0 to be the term f x.
We prove the intermediate claim Hy0def: y0 = f x.
Use reflexivity.
We prove the intermediate claim Hy0N: y0 ∈ n.
rewrite the current goal using Hy0def (from left to right).
An exact proof term for the current goal is (Hmap x HxF).
We use y0 to witness the existential quantifier.
Apply andI to the current goal.
We will prove y0 ∈ n ∧ apply_fun e y0 = x.
Apply andI to the current goal.
An exact proof term for the current goal is Hy0N.
We prove the intermediate claim Happly: apply_fun e y0 = inv F f y0.
rewrite the current goal using (apply_fun_graph n (λy : set ⇒ inv F f y) y0 Hy0N) (from left to right).
Use reflexivity.
rewrite the current goal using Happly (from left to right).
rewrite the current goal using Hy0def (from left to right).
An exact proof term for the current goal is (inj_linv F f Hinj x HxF).
Let y' be given.
Assume Hy'N: y' ∈ n.
Assume Heq: apply_fun e y' = x.
We will prove y' = y0.
We prove the intermediate claim Happly': apply_fun e y' = inv F f y'.
rewrite the current goal using (apply_fun_graph n (λy : set ⇒ inv F f y) y' Hy'N) (from left to right).
Use reflexivity.
We prove the intermediate claim HinvEq: inv F f y' = x.
rewrite the current goal using Happly' (from right to left).
An exact proof term for the current goal is Heq.
We prove the intermediate claim Hfeq: f (inv F f y') = f x.
rewrite the current goal using HinvEq (from left to right).
Use reflexivity.
We prove the intermediate claim Hfy': f (inv F f y') = y'.
An exact proof term for the current goal is (andER (inv F f y' ∈ F) (f (inv F f y') = y') (Hrinv y' Hy'N)).
We prove the intermediate claim HyEq: y' = f x.
rewrite the current goal using Hfy' (from right to left).
An exact proof term for the current goal is Hfeq.
rewrite the current goal using Hy0def (from left to right).
An exact proof term for the current goal is HyEq.
∎