proposition: Lemma decode_encode {X : Type} (HX : forall (x y : X), {x = y} + {x <> y}) {L : list X} (HL : forall x, In x L) (x : X) : decode L (encode HX HL x) = x.
proof: Proof. exact: (svalP (encode_sig HX HL x)). Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun