fact: Definition rseq_precondition r env un l := match comp_rseq r env with | None => False | Some vn => match comp_limit r env with | None => False | Some v => (un == vn) /\ (l = v) end end.
imports: Rbase MyRIneq Rsequence_def Rsequence_facts Rsequence_cv_facts List Option Tactics