proposition: Fact bsm_state_enc_fun (v : vec (list bool) m) w1 w2 : bsm_state_enc v w1 -> bsm_state_enc v w2 -> w1 = w2.
proof: Proof. Proof using cases. intros (H0 & H1 & H2 & H3) (H4 & H5 & H6 & H7). apply vec_pos_ext; intros p. destruct (cases p) as [ [ [ -> | -> ] | -> ] | (q & ->) ]; try lia. now rewrite H3, H7. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss compiler_correction) Undecidability.StackMachines.BSM(bsm_defs) Undecidability.MinskyMachines.MM(mm_defs mm_utils)