proposition: Theorem paco_acc: forall l r (OBG: forall rr (INC: r <1= rr) (CIH: l <1= rr), l <1= paco gf rr), l <1= paco gf r.
proof: Proof. intros; assert (SIM: paco gf (r \1/ l) x0) by eauto. clear PR; repeat (try left; do 2 paco_revert; paco_cofix_auto). Qed.
imports: Paco(pacotac_internal paconotation_internal)