proposition: Lemma enc_pair_match {T : Type} {P Q : T} n m : match enc_pair n m with | 0 => P | S _ => Q end = Q.
proof: Proof. have ? := Nat.pow_nonzero 2 n. suff: enc_pair n m = S (enc_pair n m - 1) by move=> ->. rewrite /enc_pair. nia. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA L.L) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability(MinskyMachines.Util.MMA_pairing L.AbstractMachines.wCBV) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun