proposition: Lemma rclo0_mon_gen clo clo' r r' (IN: @rclo0 clo r) (LEclo: clo <1= clo') (LEr: r <0= r') : @rclo0 clo' r'.
proof: Proof. induction IN; intros. - econstructor 1. apply LEr, IN. - econstructor 2; [intros; eapply H, PR|apply LEclo, IN]. Qed.
imports: Program.Basics Paco(paco0 pacotac)