Formalisation of "Axiomatic Set Theory in Type Theory" by Gert Smolka
• Version: 16 May 2015
• Author: Dominik Kirst, Saarland University
• This file covers Sections 2, 6 and 7 of the paper

Global Set Implicit Arguments.
Global Unset Strict Implicit.

Require Export Classical_Pred_Type Classical_Prop.

Ltac indirect :=
match goal with
| [ |- ?H ] => destruct (classic H); auto; exfalso
end.

# Well-Orderings in Type Theory

Notation for sub-classes and sub-orderings

Notation "p '<<=' q" := (forall x, p x -> q x) (at level 70).
Notation "p '===' q" := (p <<= q /\ q <<= p) (at level 70).
Notation "R 'o=' S" := (forall x y, R x y -> S x y) (at level 70).
Notation "R 'o=o' S" := (R o= S /\ S o= R) (at level 70).

Lemma sub_trans1 X (p: X -> Prop) q r:
p <<= q -> q <<= r -> p <<= r.
Proof.
auto.
Qed.

Lemma sub_trans2 X Y (R: X -> Y -> Prop) S T:
R o= S -> S o= T -> R o= T.
Proof.
auto.
Qed.

Definitions for binary relations

Definition inv X Y (U: X -> Y -> Prop) x y :=
U y x.

Definition dom X Y (U: X -> Y -> Prop) x :=
exists y, U x y.

Definition functional X Y (U: X -> Y -> Prop) :=
forall x y y', U x y -> U x y' -> y = y'.

Definition expansion X Y (U: X -> Y -> Prop) a b :=
fun x y => U x y \/ x = a /\ y = b.

Lemma inv_sub X Y (U: X -> Y -> Prop) (V: X -> Y -> Prop):
U o= V -> (inv U) o= (inv V).
Proof.
firstorder.
Qed.

## Theory of Well-Orderings

Definitions for orderings

Definition reflexive X (R: X -> X -> Prop) :=
forall x y, R x y -> R x x /\ R y y.

Definition antisym X (R: X -> X -> Prop) :=
forall x y, R x y -> R y x -> x = y.

Definition transitive X (R: X -> X -> Prop) :=
forall x y z, R x y -> R y z -> R x z.

Definition linear X (R: X -> X -> Prop) :=
forall x y, dom R x -> dom R y -> R x y \/ R y x.

Definition porder X (R: X -> X -> Prop) :=
reflexive R /\ antisym R /\ transitive R.

Definition Least X (R: X -> X -> Prop) p x :=
p x /\ forall y, p y -> R x y.

Definition Segs X (R: X -> X -> Prop) (p: X -> Prop) :=
(p <<= dom R) /\ (forall x y, R x y -> p y -> p x).

Definition Seg X (R: X -> X -> Prop) x y :=
R y x /\ x <> y.

Definition res X (R: X -> X -> Prop) p x y :=
p x /\ p y /\ R x y.

Definition least_inhab X (R: X -> X -> Prop) :=
forall (p: X -> Prop), ex p -> p <<= dom R -> ex (Least R p).

Definition worder X (R: X -> X -> Prop) :=
porder R /\ least_inhab R.

Definition res_seg X (R: X -> X -> Prop) a x y :=
(Seg R a) x /\ (Seg R a) y /\ R x y.

Lemma res_sub1 X (R: X -> X -> Prop) p:
dom (res R p) <<= dom R.
Proof.
firstorder.
Qed.

Lemma res_sub2 X (R: X -> X -> Prop) p:
dom (res R p) <<= p.
Proof.
firstorder.
Qed.

Lemma res_sub X (R: X -> X -> Prop) (p: X -> Prop) x:
worder R -> p x -> dom R x -> dom (res R p) x.
Proof.
firstorder.
Qed.

Lemma seg_segs X (R: X -> X -> Prop) x:
worder R -> dom R x -> Segs R (Seg R x).
Proof.
intros [[_[R1 R2]] _] DX. split.
- intros y [Y _]. now exists x.
- intros y z YZ [X1 X2]. split.
+ now apply (R2 y z x).
+ intros XY. subst. apply X2. now apply R1.
Qed.

Lemma least_inhab_linear X (R: X -> X -> Prop):
least_inhab R -> linear R.
Proof.
intros H x y XD YD.
destruct (H (fun z => x = z \/ y = z)) as [z[[Z1|Z1] Z2]]; subst.
- exists x. now left.
- intros z [Z|Z]; subst; assumption.
- left. apply (Z2 y). now right.
- right. apply (Z2 x). now left.
Qed.

Lemma worder_linear X (R: X -> X -> Prop):
worder R -> linear R.
Proof.
intros H. apply least_inhab_linear. apply H.
Qed.

Lemma linear_Segs X (R: X -> X -> Prop) p q:
linear R -> Segs R p -> Segs R q -> p <<= q \/ q <<= p.
Proof.
intros RL [P1 P2] [R1 R2]. indirect. apply not_or_and in H as [H1 H2].
apply not_all_ex_not in H1 as [x H1]. apply imply_to_and in H1.
apply not_all_ex_not in H2 as [y H2]. apply imply_to_and in H2.
destruct (RL x y); firstorder.
Qed.

Lemma worder_Segs X (R: X -> X -> Prop) p:
worder R -> Segs R p -> (p === dom R) \/ (exists x, dom R x /\ p === Seg R x).
Proof.
intros [H1 H2] [H3 H4].
destruct (classic (p === dom R)) as [H|H]; auto.
assert (LR: linear R) by now apply least_inhab_linear.
apply not_and_or in H as [H|H]; try contradiction.
apply not_all_ex_not in H.
destruct (H2 (fun x => ~(dom R x -> p x)) H) as [x[X1 X2]].
- intros x XP. now apply imply_to_and in XP.
- right. exists x. apply imply_to_and in X1 as [X1 X3].
split; try assumption. split; intros y Y.
+ split; try (intros I; now subst).
destruct (LR x y) as [XY|YX]; auto. contradict X3. now apply (H4 x y).
+ indirect. apply Y. apply H1; try apply Y. apply X2.
intros I. apply H0. apply I. exists y. firstorder.
Qed.

Lemma worder_sub X (R: X -> X -> Prop) p:
worder R -> worder (res R p).
Proof.
intros [[H1[H2 H3]]H4]. repeat split;
try apply (H1 x y); try apply H; try apply H0.
- firstorder.
- apply (H3 x y z); firstorder.
- intros q [x Q] D. destruct (H4 (fun z => q z /\ p z)) as [y Y]; firstorder.
Qed.

Lemma worder_equiv X (R: X -> X -> Prop) (S: X -> X -> Prop):
worder R -> R o=o S -> worder S.
Proof.
intros [[R1[R2 R3]] R4] RS. repeat split.
- apply RS. apply RS in H. now apply (R1 x y).
- apply RS. apply RS in H. now apply (R1 x y).
- firstorder.
- intros x y z XY YZ. apply RS. apply RS in XY.
apply RS in YZ. now apply (R3 x y z).
- intros p PI PS. destruct (R4 p PI) as [x XL].
+ intros x PX. destruct (PS x PX) as [y Y]. apply RS in Y. now exists y.
+ exists x. firstorder.
Qed.

Well-founded induction (9)

Inductive W X (R: X -> X -> Prop) x: Prop :=
| WI: Seg R x <<= W R -> W R x.

Definition wfounded X (R: X -> X -> Prop) :=
dom R <<= W R.

Lemma worder_wfounded X (R: X -> X -> Prop):
worder R -> wfounded R.
Proof.
intros [H1 H2]. indirect.
apply not_all_ex_not in H as [x XL].
apply imply_to_and in XL as [X1 X2].
destruct (H2 (fun y => dom R y /\ ~ W R y)) as [y[Y1 Y2]].
- exists x. now split.
- tauto.
- apply Y1. constructor. intros z Z. indirect. apply Z.
apply H1; try apply Z. apply Y2. split; firstorder.
Qed.

## Similarities and Isomorphisms

Definitions of Similarities

Definition simulative X Y (U: X -> Y -> Prop) R S :=
forall x x' y, U x y -> R x' x -> exists y', U x' y' /\ S y' y.

Definition simulation X Y (U: X -> Y -> Prop) R S :=
dom U <<= dom R /\ simulative U R S.

Definition similarity X Y (U: X -> Y -> Prop) R S :=
simulation U R S /\ functional U /\
simulation (inv U) S R /\ functional (inv U).

Definition isomorphism X Y (U: X -> Y -> Prop) R S :=
similarity U R S /\ dom R <<= dom U /\ dom S <<= dom (inv U).

Definition simi X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) :=
exists U, isomorphism U R S.

Definition maxisim X Y (U: X -> Y -> Prop) R S :=
similarity U R S /\ (dom R <<= dom U \/ dom S <<= dom (inv U)).

Definition Canon X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) x y :=
exists U, similarity U R S /\ U x y.

Lemma simi_inv X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
similarity U R S -> similarity (inv U) S R.
Proof.
firstorder.
Qed.

Lemma iso_inv X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
isomorphism U R S -> isomorphism (inv U) S R.
Proof.
firstorder.
Qed.

Lemma simi_simu1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
similarity U R S -> simulative U R S.
Proof.
firstorder.
Qed.

Lemma simi_simu2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
similarity U R S -> simulative (inv U) S R.
Proof.
firstorder.
Qed.

Lemma simi_com X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
simi R S -> simi S R.
Proof.
intros [U[U1 U2]]. exists (inv U). split; firstorder.
Qed.

Lemma simulation_dom X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
simulation U R S -> Segs R (dom U).
Proof.
intros [H1 H2]. split; trivial. intros x' x XX [y H].
destruct (H2 x x' y H XX) as [y' [I _]]. now exists y'.
Qed.

Lemma simi_eq1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U x y x' y':
similarity U R S -> U x y -> U x' y' -> x = x' -> y = y'.
Proof.
intros SU H1 H2 H. subst x'. firstorder.
Qed.

Lemma simi_eq2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U x y x' y':
similarity U R S -> U x y -> U x' y' -> y = y' -> x = x'.
Proof.
intros SU H1 H2 H. subst y'. firstorder.
Qed.

Lemma simi_neq1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U x y x' y':
similarity U R S -> U x y -> U x' y' -> y <> y' -> x <> x'.
Proof.
intros SU H1 H2 H3 H4. apply H3. eauto using simi_eq1.
Qed.

Lemma simi_neq2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U x y x' y':
similarity U R S -> U x y -> U x' y' -> x <> x' -> y <> y'.
Proof.
intros SU H1 H2 H3 H4. apply H3. eauto using simi_eq2.
Qed.

Lemma simi_rewrite X Y (R: X -> X -> Prop) (S S': Y -> Y -> Prop) U:
similarity U R S -> S o=o S' -> similarity U R S'.
Proof.
intros SU SS. repeat split; try apply SU.
- intros x x' y XY XX. destruct (simi_simu1 SU XY XX) as [y'[Y1 Y2]].
exists y'. split; trivial. now apply SS.
- intros x XD. apply SU in XD as [y YD]. exists y. now apply SS.
- intros x x' y XY XX. apply SS in XX.
destruct (simi_simu2 SU XY XX) as [y'[Y1 Y2]]. exists y'. split; trivial.
Qed.

Facts about domains and restrictions of similarities (13)

Lemma simi_dom1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
similarity U R S -> Segs R (dom U).
Proof.
intros [H _]. apply (simulation_dom H).
Qed.

Lemma simi_dom2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
similarity U R S -> Segs S (dom (inv U)).
Proof.
intros [_[_[H _]]]. apply (simulation_dom H).
Qed.

Lemma similarity_res X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
worder R -> worder S ->
similarity U R S -> similarity U R (res S (dom (inv U))).
Proof.
intros WOR WOS US. repeat split; try apply US.
- assert (SU: simulative U R S) by apply US.
intros x x' y UX RX. destruct (SU x x' y UX RX) as [y'[Y1 Y2]].
exists y'. split; firstorder.
- intros x XD. assert (XS: dom S x) by now apply US.
destruct XS as [y XY]. exists x. repeat split; trivial.
destruct WOS as [[SR _]_]. now apply (SR x y).
- assert (SU: simulative (inv U) S R) by apply US.
intros y y' x UY [_ [_ SY]]. destruct (SU y y' x UY SY) as [x'[X1 X2]].
exists x'. split; assumption.
Qed.

Lemma simi_res X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
worder R -> worder S ->
similarity U R S -> dom U === dom R -> isomorphism U R (res S (dom (inv U))).
Proof.
intros WOR WOS US H. split; auto using similarity_res.
split; try apply H. firstorder.
Qed.

Lemma similarity_res' X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
worder R -> worder S ->
similarity U R S -> similarity U (res R (dom U)) S.
Proof.
intros WOR WOS US. repeat split; try apply US.
- intros x XD. assert (XS: dom R x) by now apply US.
destruct XS as [y XY]. exists x. repeat split; trivial.
destruct WOR as [[RR _]_]. now apply (RR x y).
- assert (SU: simulative U R S) by apply US.
intros x x' y UX [_ [_ RX]]. destruct (SU x x' y UX RX) as [y'[Y1 Y2]].
exists y'. split; assumption.
- assert (SU: simulative (inv U) S R) by apply US.
intros y y' x UY SY. destruct (SU y y' x UY SY) as [x'[X1 X2]].
exists x'. split; firstorder.
Qed.

Lemma simi_res' X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
worder R -> worder S ->
similarity U R S -> dom (inv U) === dom S -> isomorphism U (res R (dom U)) S.
Proof.
intros WOR WOS US H. split; auto using similarity_res'.
split; try apply H. firstorder.
Qed.

Agreement and linearity of similarities (14)

Lemma simi_wfounded X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U x y:
worder R -> worder S ->
similarity U R S -> U x y -> W R x.
Proof.
intros WOR WOS SU XY. apply worder_wfounded; trivial. apply SU. now exists y.
Qed.

Lemma simi_agree X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U V x y y':
worder R -> worder S ->
similarity U R S -> similarity V R S -> U x y -> V x y' -> y = y'.
Proof.
intros WOR WOS SU SV XY.
assert (H: W R x) by apply (simi_wfounded WOR WOS SU XY).
revert y XY y'. induction H as [x H IH]. intros y XY y' XY'.
indirect. destruct (@worder_linear Y S WOS y y').
- apply SU. now exists x.
- apply SV. now exists x.
- destruct (simi_simu2 SV XY' H1) as [x'[X1 X2]].
destruct (simi_simu1 SU XY X2) as [z[Z1 Z2]].
assert (XX': x <> x') by eauto using simi_neq1.
assert (ZY': y <> z) by eauto using simi_neq2.
apply ZY'. symmetry. apply (IH x'); firstorder.
- destruct (simi_simu2 SU XY H1) as [x'[X1 X2]].
destruct (simi_simu1 SV XY' X2) as [z[Z1 Z2]].
assert (XX': x <> x') by eauto using simi_neq1.
assert (ZY': z <> y') by eauto using simi_neq2.
apply ZY'. symmetry. apply (IH x'); firstorder.
Qed.

Lemma simi_domain_sub X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U V:
worder R -> worder S ->
similarity U R S -> similarity V R S -> dom U <<= dom V -> U o= V.
Proof.
intros WOR WOS SU SV UV x y XY. destruct (UV x) as [y' H].
- now exists y.
- now rewrite (simi_agree WOR WOS SU SV XY H).
Qed.

Lemma simi_lin X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U V:
worder R -> worder S ->
similarity U R S -> similarity V R S -> U o= V \/ V o= U.
Proof.
intros WOR WOS SU SV. assert (LR: linear R) by now apply worder_linear.
destruct (linear_Segs LR (simi_dom1 SU) (simi_dom1 SV)) as [H|H].
- left. now apply (simi_domain_sub WOR WOS).
- right. now apply (simi_domain_sub WOR WOS).
Qed.

Lemma maxi_sub X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U V:
worder R -> worder S -> similarity U R S -> maxisim V R S -> U o= V.
Proof.
intros WOR WOS SU [SV[M|M]].
- apply (simi_domain_sub WOR WOS); trivial.
apply (@sub_trans1 X (dom U) (dom R)); trivial. apply SU.
- apply inv_sub. apply (simi_domain_sub WOS WOR); try now apply simi_inv.
apply (@sub_trans1 Y (dom (inv U)) (dom S)); trivial. apply SU.
Qed.

Embedding theorem (15)

Lemma canon_simulative1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
simulative (Canon R S) R S.
Proof.
intros x x' y [U[SU XY]] XX.
assert (SS: simulative U R S) by apply SU.
destruct (SS x x' y XY XX) as [y'[Y1 Y2]].
exists y'. split; trivial. exists U. now split.
Qed.

Lemma canon_simulative2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
simulative (inv (Canon R S)) S R.
Proof.
intros x x' y [U[SU XY]] XX.
assert (SS: simulative (inv U) S R) by apply SU.
destruct (SS x x' y XY XX) as [y'[Y1 Y2]].
exists y'. split; trivial. exists U. now split.
Qed.

Lemma canon_simi X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
worder R -> worder S -> similarity (Canon R S) R S.
Proof.
intros WOR WOS. repeat split.
- firstorder.
- apply canon_simulative1.
- intros x y y' [U[SU XY]] [V[SV XY']].
apply (simi_agree WOR WOS SU SV XY XY').
- firstorder.
- apply canon_simulative2.
- intros x y y' [U[SU XY]] [V[SV XY']].
apply simi_inv in SU. apply simi_inv in SV.
apply (simi_agree WOS WOR SU SV XY XY').
Qed.

Lemma exp_simulative1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U a b:
worder R -> worder S -> similarity U R S ->
Least R (fun c => dom R c /\ ~ dom U c) a ->
Least S (fun c => dom S c /\ ~ dom (inv U) c) b ->
simulative (expansion U a b) R S.
Proof.
intros WR WS [[U1 U2][U3[[U4 U5] U6]]] [[RA UA] A] [[SB UB] B].
intros x x' y [XY|[XA YB]] XX; subst.
- destruct (U2 x x' y XY XX) as [y'[Y1 Y2]]. exists y'. firstorder.
- destruct (classic (dom U x')) as [[y XY]|H].
+ exists y. split; try now left.
destruct (worder_linear WS (x:=y) (y:=b)); auto. apply U4. now exists x'.
assert (US: similarity U R S) by firstorder.
exfalso. apply UB. destruct (simi_dom2 US) as [_ SU].
apply (SU b y); trivial. now exists x'.
+ exists b. split; try apply B; auto. right. split; trivial.
apply WR; trivial. apply A. split; trivial. now exists a.
Qed.

Lemma exp_simulative2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U a b:
worder R -> worder S -> similarity U R S ->
Least R (fun c => dom R c /\ ~ dom U c) a ->
Least S (fun c => dom S c /\ ~ dom (inv U) c) b ->
simulative (inv (expansion U a b)) S R.
Proof.
intros WR WS [[U1 U2][U3[[U4 U5] U6]]] [[RA UA] A] [[SB UB] B].
intros x x' y [XY|[XA YB]] XX; subst.
- destruct (U5 x x' y XY XX) as [y'[Y1 Y2]]. exists y'. firstorder.
- destruct (classic (dom (inv U) x')) as [[y XY]|H].
+ exists y. split; try now left.
destruct (worder_linear WR (x:=y) (y:=a)); auto. apply U1. now exists x'.
assert (US: similarity U R S) by firstorder.
exfalso. apply UA. destruct (simi_dom1 US) as [_ SU].
apply (SU a y); trivial. now exists x'.
+ exists a. split; try apply B; auto. right. split; trivial.
apply WS; trivial. apply B. split; trivial. now exists b.
Qed.

Lemma exp_simi X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U a b:
worder R -> worder S -> similarity U R S ->
Least R (fun c => dom R c /\ ~ dom U c) a ->
Least S (fun c => dom S c /\ ~ dom (inv U) c) b ->
similarity (expansion U a b) R S.
Proof.
intros WR WS [[U1 U2][U3[[U4 U5] U6]]] [[RA UA] A] [[SB UB] B]. repeat split.
- intros x [y[H|[H1 H2]]]; subst; auto. apply U1. now exists y.
- apply exp_simulative1; firstorder.
- intros x y y' [XY|[XA YB]] [XY'|[XA' YB']]; subst; eauto.
+ contradict UA. now exists y.
+ contradict UA. now exists y'.
- intros x [y[H|[H1 H2]]]; subst; auto. apply U4. now exists y.
- apply exp_simulative2; firstorder.
- intros x y y' [XY|[XA YB]] [XY'|[XA' YB']]; subst; eauto.
+ contradict UB. now exists y.
+ contradict UB. now exists y'.
Qed.

Lemma canon_max X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
worder R -> worder S -> maxisim (Canon R S) R S.
Proof.
intros WOR WOS. split; try now apply canon_simi.
indirect. apply not_or_and in H as [H1 H2].
apply not_all_ex_not in H1 as [a' A]. apply imply_to_and in A as [A1 A2].
apply not_all_ex_not in H2 as [b' B]. apply imply_to_and in B as [B1 B2].
assert (RL: least_inhab R) by now apply WOR.
destruct (RL (fun c => dom R c /\ ~ dom (Canon R S) c)) as [a A].
exists a'. now split. tauto.
assert (SL: least_inhab S) by now apply WOS.
destruct (SL (fun c => dom S c /\ ~ dom (inv (Canon R S)) c)) as [b B].
exists b'. now split. tauto.
apply A. exists b. exists (expansion (Canon R S) a b). split.
- apply exp_simi; auto using canon_simi.
- now right.
Qed.

Lemma canon_unique X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
worder R -> worder S -> maxisim U R S -> U o=o Canon R S.
Proof.
intros WOR WOS MU. split.
- apply (maxi_sub WOR WOS); auto using canon_max. apply MU.
- apply (maxi_sub WOR WOS); auto using canon_simi.
Qed.

Lemma embedding X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
worder R -> worder S ->
(exists p, Segs R p /\ simi (res R p) S) \/
(exists q, Segs S q /\ simi R (res S q)).
Proof.
intros WOR WOS. destruct (canon_max WOR WOS) as [C1[C2|C2]].
- right. exists (dom (inv (Canon R S))). split.
+ apply (simi_dom2 C1).
+ exists (Canon R S). apply (simi_res WOR WOS C1). firstorder.
- left. exists (dom (Canon R S)). split.
+ apply (simi_dom1 C1).
+ exists (Canon R S). apply (simi_res' WOR WOS C1). firstorder.
Qed.

Segments are equivalent iff they are isomorphic (16)

Lemma seg_equal X (R: X -> X -> Prop) x y:
worder R -> dom R x -> dom R y -> Seg R x === Seg R y -> x = y.
Proof.
intros WOR DX DY [XY YX]. indirect.
assert (LR: linear R) by now apply worder_linear.
destruct (LR x y DX DY) as [I|I].
- apply (YX x); firstorder.
- apply (XY y); firstorder.
Qed.

Lemma simi_sub X (R: X -> X -> Prop) p q:
worder R -> Segs R p -> Segs R q -> simi (res R p) (res R q) -> p <<= q.
Proof.
intros WOR SP SQ [U[U1[U2 U3]]]. cut (forall x, dom (res R p) x -> U x x).
- intros H x PX. assert (UX: dom U x).
+ apply U2. apply res_sub; firstorder.
+ apply (res_sub2 (R:=R)). apply U1. exists x. apply H. now apply U1.
- assert (WR: wfounded R) by now apply worder_wfounded.
intros x DX. assert (XR: dom R x) by now apply (res_sub1 (p:=p)).
specialize (WR x XR). induction WR as [x H IH].
destruct (U2 x DX) as [y Y]. cut (x = y); try congruence.
destruct U1 as [[H1 H2][H3[[H4 H5]H6]]]. apply (seg_equal WOR); auto.
+ apply (res_sub1 (p:=q)). apply H4. now exists x.
+ split; intros z Z.
* assert (ZX: res R p z x) by firstorder.
destruct (H2 x z y Y) as [z'[Z1' Z2']]; trivial.
assert (ZD1: dom (res R p) z) by now exists x.
assert (ZD2: dom R z) by (exists x; apply Z).
specialize (IH z Z ZD1 ZD2). rewrite (H3 z z z' IH Z1').
split; try apply Z2'. intros YZ. subst.
apply Z. now apply (H6 z').
* assert (DY: dom (inv U) y) by now exists x.
assert (QY: q y) by apply (res_sub2 (H4 y DY)).
assert (ZX: res R q z y) by firstorder.
destruct (H5 y z x Y) as [z'[Z1' Z2']]; trivial.
assert (ZD1: dom (res R p) z') by now exists x.
assert (ZD2: dom R z') by (exists x; apply Z2').
assert (Z': Seg R x z'). { split. apply Z2'. intros J. subst.
apply Z. now apply (H3 z' y z). }
specialize (IH z' Z' ZD1 ZD2). rewrite (H3 z' z z' Z1' IH).
split; try apply Z2'. intros YZ. subst. now apply Z'.
Qed.

Lemma simi_equiv X (R: X -> X -> Prop) p q:
worder R -> Segs R p -> Segs R q -> simi (res R p) (res R q) -> p === q.
Proof.
intros WOR SP SQ PQ. split.
- now apply (simi_sub WOR).
- apply (simi_sub WOR); auto using simi_com.
Qed.

Lemma equiv_simi X (R: X -> X -> Prop) p q:
worder R -> Segs R p -> Segs R q -> p === q -> simi (res R p) (res R q).
Proof.
intros WOR SP SQ PQ. exists (fun x y => p x /\ x = y). repeat split.
- intros x [y[H1 H2]]. subst y. exists x. repeat split; firstorder.
- intros x x' y [X1 X2] XY. subst y. exists x'. repeat split; firstorder.
- intros x y y' [_ XY] [_ XY']. congruence.
- intros x [y[H1 H2]]. subst y. exists x. repeat split; firstorder.
- intros x x' y [X1 X2] XY. subst y. exists x'. repeat split; firstorder.
- intros x y y' [_ XY] [_ XY']. congruence.
- intros x [y[H1 H2]]. exists x. now split.
- intros x [y[H1 H2]]. exists x. apply PQ in H1. now split.
Qed.

Lemma simi_trans X (R: X -> X -> Prop) (S1: X -> X -> Prop) (S2: X -> X -> Prop):
simi R S1 -> simi R S2 -> simi S1 S2.
Proof.
intros [U[[[H1 H2][H3[[H4 H5] H6]]][H7 H8]]].
intros [V[[[I1 I2][I3[[I4 I5] I6]]][I7 I8]]].
pose (W := fun x z => exists y, U y x /\ V y z).
exists W. repeat split.
- firstorder.
- intros x x' y [z[Z1 Z2]] XX. destruct (H5 x x' z Z1 XX) as [z'[Z3 Z4]].
destruct (I2 z z' y Z2 Z4) as [y'[Y1 Y2]]. exists y'. firstorder.
- intros x y y' [z[Z1 Z2]] [z'[Z3 Z4]]. apply (I3 z y y'); trivial.
cutrewrite (z = z'); trivial. now apply (H6 x z z').
- firstorder.
- intros x x' y [z[Z1 Z2]] XX. destruct (I5 x x' z Z2 XX) as [z'[Z3 Z4]].
destruct (H2 z z' y Z1 Z4) as [y'[Y1 Y2]]. exists y'. firstorder.
- intros x y y' [z[Z1 Z2]] [z'[Z3 Z4]]. apply (H3 z y y'); trivial.
cutrewrite (z = z'); trivial. now apply (I6 x z z').
- intros x XD. destruct (H8 x XD) as [z Z]. assert (H: dom U z) by now exists x.
destruct (I7 z (H1 z H)) as [y Y]. exists y. exists z. split; assumption.
- intros x XD. destruct (I8 x XD) as [z Z]. assert (H: dom V z) by now exists x.
destruct (H7 z (I1 z H)) as [y Y]. exists y. exists z. split; assumption.
Qed.