proposition: Theorem reduction : SSemiU ⪯ RU2SemiU.
proof: Proof. exists (fun p => (Argument.σ false p, Argument.σ true p, Argument.τ p)). intro p. constructor. - exact Argument.transport. - exact Argument.reflection. Qed.
imports: List Undecidability.SemiUnification.SemiU Undecidability.SemiUnification.Util(Enumerable) ssreflect ssrfun ssrbool Undecidability.Synthetic.Definitions