proposition: Lemma gpaco12_uclo uclo clo r rg (LEclo: uclo <13= gupaco12 clo) : uclo (gpaco12 clo r rg) <12= gpaco12 clo r rg.
proof: Proof. intros. apply gpaco12_gupaco. apply LEclo, PR. Qed.
imports: Program.Basics Paco(paco12 pacotac)