proposition: Lemma gpaco10_uclo uclo clo r rg (LEclo: uclo <11= gupaco10 clo) : uclo (gpaco10 clo r rg) <10= gpaco10 clo r rg.
proof: Proof. intros. apply gpaco10_gupaco. apply LEclo, PR. Qed.
imports: Program.Basics Paco(paco10 pacotac)