proposition: Lemma sos_step_f_sos : forall r i i' r', sos_step r i i' r' -> f_sos r i = Some(r', i').
proof: Proof. Proof with eauto. induction 1... unfold f_sos, bind... match goal with id : _ |- _ => rewrite aeval_f with (1:=id) end. match goal with id : _ |- _ => rewrite s_update_f with (1:=id) end... simpl. case (eq_skip i1). intros; subst; inversion H. intros; rewrite IHsos_step; eauto. simpl; match goal with id :_ |- _ => rewrite beval_f with (1:=id); auto end. simpl; match goal with id :_ |- _ => rewrite beval_f with (1:=id); auto end. Qed.
imports: ZArith List syntax Lia