proposition: Lemma gpaco11_uclo uclo clo r rg (LEclo: uclo <12= gupaco11 clo) : uclo (gpaco11 clo r rg) <11= gpaco11 clo r rg.
proof: Proof. intros. apply gpaco11_gupaco. apply LEclo, PR. Qed.
imports: Program.Basics Paco(paco11 pacotac)