proposition: Lemma paco14_mon_bot (gf gf': rel14 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 -> rel14 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13) r' x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 (REL: paco14 gf bot14 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) (LEgf: gf <15= gf'): paco14 gf' r' x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13.
proof: Proof. eapply paco14_mon_gen; [apply REL | apply LEgf | intros; contradiction PR]. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)