Require Import Coq.Program.Equality.
Require Import Coq.Unicode.Utf8_core.

Reserved Notation "r ≤ s" (at level 70, no associativity).

Inductive Ord : Type :=
| suc : Ord Ord
| lim : {A : Type}, (A Ord) Ord.

Inductive Leq : Ord Ord Prop :=
| mono : {r s}, r s suc r suc s
| cocone : {s A f}, ( (a : A), s f a) s lim f
| limiting : {s A f}, ( (a : A), f a s) lim f s
where "r ≤ s" := (Leq r s).

Definition Lt (r s : Ord) : Prop := suc r s.
Notation "r < s" := (Lt r s).

Property reflLeq (s : Ord) : s s. Admitted.
Property transLeq {r s t : Ord} (rs : r s) (st : s t) : r t. Admitted.

Inductive Acc (s : Ord) : Prop :=
| acc : ( r, r < s Acc r) Acc s.

Lemma accLeq : r s, r s Acc s Acc r.
Proof.
  intros r s rs acc.
  induction acc as [s p IH].
  exact (acc r (λ t tr, p t (transLeq tr rs))).
Qed.

Theorem accOrd : s, Acc s.
Proof.
  intros s.
  induction s as [s IH | A f IH].
  - destruct IH as [p].
    refine (acc (suc s) (λ r rsucs, acc r (λ t tr, p t (transLeq tr _)))).
    inversion rsucs as [r' s' rs | |].
    exact rs.
  - refine (acc (lim f) (λ r rlimf, _)).
    inversion rlimf as [| r' A' f' erfa eqr eqA |].
    dependent destruction H.
    destruct erfa as [a rfa].
    destruct (IH a) as [p].
    exact (p r rfa).
Qed.