proposition: Lemma gpaco13_uclo uclo clo r rg (LEclo: uclo <14= gupaco13 clo) : uclo (gpaco13 clo r rg) <13= gpaco13 clo r rg.
proof: Proof. intros. apply gpaco13_gupaco. apply LEclo, PR. Qed.
imports: Program.Basics Paco(paco13 pacotac)