Prove soundness for intervalvalidator anew with correct precondition approximation assumption as in Coq Dev