proposition: Lemma gpaco13_step clo r rg: gf (gpaco13 clo rg rg) <13= gpaco13 clo r rg.
proof: Proof. intros. apply gpaco13_step_gen. eapply gf_mon. apply PR. intros. eapply gpaco13_mon. apply PR0. left; apply PR1. left; apply PR1. Qed.
imports: Program.Basics Paco(paco13 pacotac)