proposition: Lemma first_st_at_inj : forall n1 n2 A (P:A->Prop) s, first_st_at P s n1 -> first_st_at P s n2 -> n1 = n2.
proof: Proof. Proof using. induction n1; destruct n2; destruct s; simpl; introv H1 H2. auto. destruct H2. false. destruct H1. false. destruct H1. destruct H2. fequals. apply* IHn1. Qed.
imports: TLC(LibTactics LibLogic LibInt LibList LibRelation LibWf)