proposition: Lemma steps_det': forall s1 s2 h, step_star s1 h s2 -> msgid_inv s1 -> forall s3, step_star s1 h s3 -> s2 = s3.
proof: Proof. induction 1; inversion 2; intuition subst. length_contra. length_contra. apply rev_cons_invert in H3; intuition subst. apply H8 in H4; clear H8; subst. eauto using step_det, steps_msgid_inv. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)