proposition: Theorem reduction : RU2SemiU ⪯ LU2SemiU.
proof: Proof. exists (fun '(s0, s1, t) => (Argument.s' s0 s1, Argument.t0' t, Argument.t1' t)). move=> [[? ?] ?]. constructor. - move=> [?] [?] [?] [? ?]. apply: Argument.transport; by eassumption. - move=> [?] [?] [?] [? ?]. apply: Argument.reflection; by eassumption. Qed.
imports: List Undecidability.SemiUnification.SemiU Undecidability.SemiUnification.Util(Enumerable) ssreflect ssrfun ssrbool Undecidability.Synthetic.Definitions