fact: Definition mconfigAsPair {B : finType} {n} (c:mconfig sig B n):= let (x,y) := c in (x,y).
imports: Undecidability.L.Datatypes(LVector) Undecidability.L(Functions.EqBool) Undecidability.TM.Util(TM_facts) Undecidability.L.Tactics(LTactics GenEncode)