proposition: Theorem generic_compiler : compiler_t.
proof: Proof. Proof using Hilen Hicomp step_Y_fun step_X_tot. exists link code; auto. Defined.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Code(subcode sss compiler)