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. unfold le1. eapply paco_acc. Qed.
imports: Paco(pacotac_internal paconotation_internal)