proposition: Theorem reduction : CSSM_UB ⪯ SSemiU.
proof: Proof. exists (fun dM => Argument.SM_to_SUcs (proj1_sig dM)). intros [M HM]. constructor. - exact Argument.soundness. - exact Argument.completeness. Qed.
imports: List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.StackMachines(SSM) Undecidability.StackMachines.Util(CSSM_facts) Undecidability.SemiUnification.SemiU Undecidability.SemiUnification.Util(Enumerable) ssreflect ssrfun ssrbool Undecidability.Synthetic.Definitions