proposition: Lemma monotone7_union (gf gf': rel7 T0 T1 T2 T3 T4 T5 T6 -> rel7 T0 T1 T2 T3 T4 T5 T6) (MON1: monotone7 gf) (MON2: monotone7 gf'): monotone7 (gf \8/ gf').
proof: Proof. red; intros. destruct IN. - left. eapply MON1. apply H. apply LE. - right. eapply MON2. apply H. apply LE. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)