Let F, e, i and n be given.
Assume HiDom: i ∈ n.
Assume HsiDom: ordsucc i ∈ n.
Assume Hbij: bijection n F e.
We prove the intermediate claim HeFun: function_on e n F.
An exact proof term for the current goal is (andEL (function_on e n F) (∀y : set, y ∈ F → ∃x0 : set, x0 ∈ n ∧ apply_fun e x0 = y ∧ (∀x' : set, x' ∈ n → apply_fun e x' = y → x' = x0)) Hbij).
We prove the intermediate claim Huniq: ∀y : set, y ∈ F → ∃x0 : set, x0 ∈ n ∧ apply_fun e x0 = y ∧ (∀x' : set, x' ∈ n → apply_fun e x' = y → x' = x0).
An exact proof term for the current goal is (andER (function_on e n F) (∀y : set, y ∈ F → ∃x0 : set, x0 ∈ n ∧ apply_fun e x0 = y ∧ (∀x' : set, x' ∈ n → apply_fun e x' = y → x' = x0)) Hbij).
We will prove function_on (swap_adjacent e i n) n F ∧ (∀y : set, y ∈ F → ∃x0 : set, x0 ∈ n ∧ apply_fun (swap_adjacent e i n) x0 = y ∧ (∀x' : set, x' ∈ n → apply_fun (swap_adjacent e i n) x' = y → x' = x0)).
Apply andI to the current goal.
An exact proof term for the current goal is (function_on_swap_adjacent F e i n HiDom HsiDom HeFun).
Let y be given.
Assume HyF: y ∈ F.
Apply (Huniq y HyF) to the current goal.
Let x0 be given.
Assume Hx0pack.
We prove the intermediate claim Hx0AB: x0 ∈ n ∧ apply_fun e x0 = y.
An exact proof term for the current goal is (andEL (x0 ∈ n ∧ apply_fun e x0 = y) (∀x' : set, x' ∈ n → apply_fun e x' = y → x' = x0) Hx0pack).
We prove the intermediate claim Hx0Dom: x0 ∈ n.
An exact proof term for the current goal is (andEL (x0 ∈ n) (apply_fun e x0 = y) Hx0AB).
We prove the intermediate claim Hex0: apply_fun e x0 = y.
An exact proof term for the current goal is (andER (x0 ∈ n) (apply_fun e x0 = y) Hx0AB).
We prove the intermediate claim Huniq0: ∀x' : set, x' ∈ n → apply_fun e x' = y → x' = x0.
An exact proof term for the current goal is (andER (x0 ∈ n ∧ apply_fun e x0 = y) (∀x' : set, x' ∈ n → apply_fun e x' = y → x' = x0) Hx0pack).
Set x1 to be the term If_i (x0 = i) (ordsucc i) (If_i (x0 = ordsucc i) i x0).
We prove the intermediate claim Hx1Def: x1 = If_i (x0 = i) (ordsucc i) (If_i (x0 = ordsucc i) i x0).
Use reflexivity.
We prove the intermediate claim Hx1Dom: x1 ∈ n.
rewrite the current goal using Hx1Def (from left to right) at position 1.
Apply (xm (x0 = i)) to the current goal.
Assume Hx0i: x0 = i.
rewrite the current goal using (If_i_1 (x0 = i) (ordsucc i) (If_i (x0 = ordsucc i) i x0) Hx0i) (from left to right).
An exact proof term for the current goal is HsiDom.
Assume Hx0ni: ¬ (x0 = i).
rewrite the current goal using (If_i_0 (x0 = i) (ordsucc i) (If_i (x0 = ordsucc i) i x0) Hx0ni) (from left to right).
Apply (xm (x0 = ordsucc i)) to the current goal.
Assume Hx0si: x0 = ordsucc i.
rewrite the current goal using (If_i_1 (x0 = ordsucc i) i x0 Hx0si) (from left to right).
An exact proof term for the current goal is HiDom.
Assume Hx0nsi: ¬ (x0 = ordsucc i).
rewrite the current goal using (If_i_0 (x0 = ordsucc i) i x0 Hx0nsi) (from left to right).
An exact proof term for the current goal is Hx0Dom.
We prove the intermediate claim Hx1Eq: apply_fun (swap_adjacent e i n) x1 = y.
rewrite the current goal using Hx1Def (from left to right) at position 1.
Apply (xm (x0 = i)) to the current goal.
Assume Hx0i: x0 = i.
rewrite the current goal using (If_i_1 (x0 = i) (ordsucc i) (If_i (x0 = ordsucc i) i x0) Hx0i) (from left to right).
We prove the intermediate claim Happ: apply_fun (swap_adjacent e i n) (ordsucc i) = apply_fun e i.
An exact proof term for the current goal is (swap_adjacent_at_succ e i n HsiDom).
rewrite the current goal using Happ (from left to right).
rewrite the current goal using Hx0i (from right to left).
An exact proof term for the current goal is Hex0.
Assume Hx0ni: ¬ (x0 = i).
rewrite the current goal using (If_i_0 (x0 = i) (ordsucc i) (If_i (x0 = ordsucc i) i x0) Hx0ni) (from left to right).
Apply (xm (x0 = ordsucc i)) to the current goal.
Assume Hx0si: x0 = ordsucc i.
rewrite the current goal using (If_i_1 (x0 = ordsucc i) i x0 Hx0si) (from left to right).
We prove the intermediate claim Happ: apply_fun (swap_adjacent e i n) i = apply_fun e (ordsucc i).
An exact proof term for the current goal is (swap_adjacent_at_i e i n HiDom).
rewrite the current goal using Happ (from left to right).
rewrite the current goal using Hx0si (from right to left).
An exact proof term for the current goal is Hex0.
Assume Hx0nsi: ¬ (x0 = ordsucc i).
rewrite the current goal using (If_i_0 (x0 = ordsucc i) i x0 Hx0nsi) (from left to right).
We prove the intermediate claim Happ: apply_fun (swap_adjacent e i n) x0 = if x0 = i then apply_fun e (ordsucc i) else if x0 = ordsucc i then apply_fun e i else apply_fun e x0.
An exact proof term for the current goal is (swap_adjacent_apply e i n x0 Hx0Dom).
rewrite the current goal using Happ (from left to right).
rewrite the current goal using (If_i_0 (x0 = i) (apply_fun e (ordsucc i)) (if x0 = ordsucc i then apply_fun e i else apply_fun e x0) Hx0ni) (from left to right).
rewrite the current goal using (If_i_0 (x0 = ordsucc i) (apply_fun e i) (apply_fun e x0) Hx0nsi) (from left to right).
An exact proof term for the current goal is Hex0.
We use x1 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hx1Dom.
An exact proof term for the current goal is Hx1Eq.
Let x' be given.
Assume Hx'Dom: x' ∈ n.
Assume Hx'Eq: apply_fun (swap_adjacent e i n) x' = y.
We prove the intermediate claim Hx'EqE: apply_fun e (If_i (x' = i) (ordsucc i) (If_i (x' = ordsucc i) i x')) = y.
Set xu to be the term If_i (x' = i) (ordsucc i) (If_i (x' = ordsucc i) i x').
We prove the intermediate claim HxuDef: xu = If_i (x' = i) (ordsucc i) (If_i (x' = ordsucc i) i x').
Use reflexivity.
rewrite the current goal using HxuDef (from right to left).
rewrite the current goal using HxuDef (from left to right) at position 1.
Apply (xm (x' = i)) to the current goal.
Assume Hx'i: x' = i.
rewrite the current goal using (If_i_1 (x' = i) (ordsucc i) (If_i (x' = ordsucc i) i x') Hx'i) (from left to right).
We prove the intermediate claim Happ: apply_fun (swap_adjacent e i n) i = apply_fun e (ordsucc i).
An exact proof term for the current goal is (swap_adjacent_at_i e i n HiDom).
rewrite the current goal using Happ (from right to left).
rewrite the current goal using Hx'i (from right to left) at position 2.
An exact proof term for the current goal is Hx'Eq.
Assume Hx'ni: ¬ (x' = i).
rewrite the current goal using (If_i_0 (x' = i) (ordsucc i) (If_i (x' = ordsucc i) i x') Hx'ni) (from left to right).
Apply (xm (x' = ordsucc i)) to the current goal.
Assume Hx'si: x' = ordsucc i.
rewrite the current goal using (If_i_1 (x' = ordsucc i) i x' Hx'si) (from left to right).
We prove the intermediate claim Happ: apply_fun (swap_adjacent e i n) (ordsucc i) = apply_fun e i.
An exact proof term for the current goal is (swap_adjacent_at_succ e i n HsiDom).
rewrite the current goal using Happ (from right to left).
rewrite the current goal using Hx'si (from right to left).
An exact proof term for the current goal is Hx'Eq.
Assume Hx'nsi: ¬ (x' = ordsucc i).
rewrite the current goal using (If_i_0 (x' = ordsucc i) i x' Hx'nsi) (from left to right).
We prove the intermediate claim Happ: apply_fun (swap_adjacent e i n) x' = if x' = i then apply_fun e (ordsucc i) else if x' = ordsucc i then apply_fun e i else apply_fun e x'.
An exact proof term for the current goal is (swap_adjacent_apply e i n x' Hx'Dom).
We prove the intermediate claim Htmp: apply_fun (swap_adjacent e i n) x' = apply_fun e x'.
rewrite the current goal using Happ (from left to right).
rewrite the current goal using (If_i_0 (x' = i) (apply_fun e (ordsucc i)) (if x' = ordsucc i then apply_fun e i else apply_fun e x') Hx'ni) (from left to right).
rewrite the current goal using (If_i_0 (x' = ordsucc i) (apply_fun e i) (apply_fun e x') Hx'nsi) (from left to right).
Use reflexivity.
rewrite the current goal using Htmp (from right to left).
An exact proof term for the current goal is Hx'Eq.
Set xu to be the term If_i (x' = i) (ordsucc i) (If_i (x' = ordsucc i) i x').
We prove the intermediate claim HxuDef: xu = If_i (x' = i) (ordsucc i) (If_i (x' = ordsucc i) i x').
Use reflexivity.
We prove the intermediate claim Hx'u: xu ∈ n.
rewrite the current goal using HxuDef (from left to right) at position 1.
Apply (xm (x' = i)) to the current goal.
Assume Hx'i: x' = i.
rewrite the current goal using (If_i_1 (x' = i) (ordsucc i) (If_i (x' = ordsucc i) i x') Hx'i) (from left to right).
An exact proof term for the current goal is HsiDom.
Assume Hx'ni: ¬ (x' = i).
rewrite the current goal using (If_i_0 (x' = i) (ordsucc i) (If_i (x' = ordsucc i) i x') Hx'ni) (from left to right).
Apply (xm (x' = ordsucc i)) to the current goal.
Assume Hx'si: x' = ordsucc i.
rewrite the current goal using (If_i_1 (x' = ordsucc i) i x' Hx'si) (from left to right).
An exact proof term for the current goal is HiDom.
Assume Hx'nsi: ¬ (x' = ordsucc i).
rewrite the current goal using (If_i_0 (x' = ordsucc i) i x' Hx'nsi) (from left to right).
An exact proof term for the current goal is Hx'Dom.
We prove the intermediate claim HxuEq: xu = x0.
An exact proof term for the current goal is (Huniq0 xu Hx'u Hx'EqE).
rewrite the current goal using Hx1Def (from right to left).
Apply (xm (x' = i)) to the current goal.
Assume Hx'i: x' = i.
We prove the intermediate claim Hxu: xu = ordsucc i.
rewrite the current goal using HxuDef (from left to right).
rewrite the current goal using (If_i_1 (x' = i) (ordsucc i) (If_i (x' = ordsucc i) i x') Hx'i) (from left to right).
Use reflexivity.
We prove the intermediate claim Hx0si: x0 = ordsucc i.
rewrite the current goal using HxuEq (from right to left).
An exact proof term for the current goal is Hxu.
rewrite the current goal using Hx0si (from left to right) at position 1.
We prove the intermediate claim Hneq: ¬ (ordsucc i = i).
Assume Heq: ordsucc i = i.
We prove the intermediate claim Hii: i ∈ i.
rewrite the current goal using Heq (from right to left) at position 2.
An exact proof term for the current goal is (ordsuccI2 i).
An exact proof term for the current goal is ((In_irref i) Hii).
rewrite the current goal using (If_i_0 (ordsucc i = i) (ordsucc i) (If_i (x0 = ordsucc i) i x0) Hneq) (from left to right).
rewrite the current goal using (If_i_1 (x0 = ordsucc i) i x0 Hx0si) (from left to right).
rewrite the current goal using Hx'i (from right to left).
Use reflexivity.
Assume Hx'ni: ¬ (x' = i).
Apply (xm (x' = ordsucc i)) to the current goal.
Assume Hx'si: x' = ordsucc i.
We prove the intermediate claim Hxu: xu = i.
rewrite the current goal using HxuDef (from left to right).
rewrite the current goal using (If_i_0 (x' = i) (ordsucc i) (If_i (x' = ordsucc i) i x') Hx'ni) (from left to right).
rewrite the current goal using (If_i_1 (x' = ordsucc i) i x' Hx'si) (from left to right).
Use reflexivity.
We prove the intermediate claim Hx0i: x0 = i.
rewrite the current goal using HxuEq (from right to left).
An exact proof term for the current goal is Hxu.
rewrite the current goal using (If_i_1 (x0 = i) (ordsucc i) (If_i (x0 = ordsucc i) i x0) Hx0i) (from left to right).
rewrite the current goal using Hx'si (from right to left).
Use reflexivity.
Assume Hx'nsi: ¬ (x' = ordsucc i).
We prove the intermediate claim Hxu: xu = x'.
rewrite the current goal using HxuDef (from left to right).
rewrite the current goal using (If_i_0 (x' = i) (ordsucc i) (If_i (x' = ordsucc i) i x') Hx'ni) (from left to right).
rewrite the current goal using (If_i_0 (x' = ordsucc i) i x' Hx'nsi) (from left to right).
Use reflexivity.
We prove the intermediate claim Hx0x': x0 = x'.
rewrite the current goal using HxuEq (from right to left).
An exact proof term for the current goal is Hxu.
rewrite the current goal using Hx0x' (from left to right) at position 1.
rewrite the current goal using (If_i_0 (x' = i) (ordsucc i) (If_i (x0 = ordsucc i) i x0) Hx'ni) (from left to right).
rewrite the current goal using Hx0x' (from left to right) at position 1.
rewrite the current goal using (If_i_0 (x' = ordsucc i) i x0 Hx'nsi) (from left to right).
rewrite the current goal using Hx0x' (from left to right).
Use reflexivity.
∎