proposition: Lemma rclo0_dist clo (MON: monotone0 clo) (DIST: forall r1 r2, clo (r1 \0/ r2) <0= (clo r1 \0/ clo r2)): forall r1 r2, rclo0 clo (r1 \0/ r2) <0= (rclo0 clo r1 \0/ rclo0 clo r2).
proof: Proof. intros. induction PR. + destruct IN; [left|right]; apply rclo0_base, H. + assert (REL: clo (rclo0 clo r1 \0/ rclo0 clo r2)). { eapply MON. apply IN. apply H. } apply DIST in REL. destruct REL; [left|right]; apply rclo0_clo, H0. Qed.
imports: Program.Basics Paco(paco0 pacotac)