Definition t s1 s2 := s1 ~> subset.t s2.
Definition img : ∀ {s1 s2}, [knownNat s2, isSucc s1 ⇒ t s1 s2 → subset.t s1 → subset.t s2] :=
  fun _ _ r A ⇒ subset.big.union r A.

Module binary.
  Definition t s := relation.t s s.
  Definition img : ∀ {s}, [knownNat s, isSucc s ⇒ t s → subset.t s → subset.t s] := fun s ⇒ @relation.img s s.
End binary.

Require Import regexp.concrete.universe.
Require regexp.concrete.relation.
Require regexp.concrete.subset.
Require regexp.synthesis.clash.axioms.

Section Synthesis.
  Context {s1 s2 : universe.sort}.
  Definition syn (rl : concrete.relation.t s1 s2) : t ⟨ s1 ⟩ ⟨ s2 ⟩ :=
    function.syn (concrete.function.map (subset.syn) rl).

  Lemma img_spec rl (st : concrete.subset.t s1) :
    img (syn rl) (subset.syn st) = subset.syn (concrete.relation.img rl st).
    by rewrite /img /syn -axioms.map_spec bigunion_spec /concrete.relation.img.
  Qed.

End Synthesis.