proposition: Lemma cpn14_compat: compatible14 gf cpn14.
proof: Proof. econstructor; [apply cpn14_mon|intros]. destruct PR; eapply gf_mon with (r:=clo r). - eapply (compat14_compat COM); apply CLO. - intros. econstructor; [apply COM|apply PR]. Qed.
imports: Program.Basics Paco(paco14 pacotac)