proposition: Lemma run_fun: forall p b1, Run p b1 -> forall b2, Run p b2 -> b1 = b2.
proof: Proof. intros p r1 H; induction H; intros r' He; inversion He; subst; clear He; auto; repeat match goal with | [ H1: Run ?q ?b1, H2: Run ?q ?b2 |- _] => ( assert (b1 = b2) by eauto || assert (b2 = b1) by eauto ); subst; clear H2; auto end; auto. eauto using exec_fun. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop