proposition: Lemma wcompat11_union clo1 clo2 (WCMP1: wcompatible11 clo1) (WCMP2: wcompatible11 clo2): wcompatible11 (clo1 \12/ clo2).
proof: Proof. econstructor. - apply monotone11_union. apply WCMP1. apply WCMP2. - intros. destruct PR. + apply WCMP1 in H. eapply gf_mon. apply H. intros. eapply gupaco11_mon_gen. apply PR. apply gf_mon. intros; apply PR0. left; apply PR0. intros; apply PR0. + apply WCMP2 in H. eapply gf_mon. apply H. intros. eapply gupaco11_mon_gen. apply PR. apply gf_mon. intros; apply PR0. right; apply PR0. intros; apply PR0. Qed.
imports: Program.Basics Paco(paco11 pacotac)