proposition: Lemma tactic_correctness : forall r env un l, rseq_precondition r env un l -> is_limit un l.
proof: Proof. unfold rseq_precondition ; intros r env un l ; destruct (comp_rseq r env) eqn:E; symmetry in E; destruct (comp_limit r env) eqn:E'; symmetry in E'; intros []. intros ; eapply is_limit_ext ; [ eapply comp_rseq_limit_compat | |] ; symmetry ; eassumption. Qed.
imports: Rbase MyRIneq Rsequence_def Rsequence_facts Rsequence_cv_facts List Option Tactics