proposition: Lemma compat1_compatible' clo (COM: compatible1 gf clo): compatible'1 clo.
proof: Proof. destruct COM. econstructor; [apply compat1_mon0|]. intros. split. - eapply compat1_mon0; intros; [apply PR| apply PR0]. - apply compat1_compat0. eapply compat1_mon0; intros; [apply PR| apply PR0]. Qed.
imports: Program.Basics Paco(paco1 pacotac)