Require Import List.
Import ListNotations.

Require Import Undecidability.SemiUnification.SemiU.

Require Import ssreflect ssrfun ssrbool.

Require Import Undecidability.Synthetic.Definitions.

Theorem reduction : RU2SemiU ⪯ SemiU.
Proof.
  exists (fun '(s0, s1, t) => [(s0, t); (s1, t)]).
  move=> [[s0 s1] t]. constructor.
  - move=> [φ] [ψ0] [ψ1] [Hψ0 Hψ1]. exists φ.
    apply /Forall_forall.
    by constructor; [by exists ψ0 | constructor; [by exists ψ1|]].
  - move=> [φ].
    move=> /Forall_forall /Forall_cons_iff [[ψ0 Hψ0]] /Forall_cons_iff [[ψ1 Hψ1]] _.
    by exists φ, ψ0, ψ1.
Qed.