proposition: Lemma gpaco14_uclo uclo clo r rg (LEclo: uclo <15= gupaco14 clo) : uclo (gpaco14 clo r rg) <14= gpaco14 clo r rg.
proof: Proof. intros. apply gpaco14_gupaco. apply LEclo, PR. Qed.
imports: Program.Basics Paco(paco14 pacotac)